TheoremslowerClosure, of_lowerClosure, of_upperClosure, upperClosure, maximal_mem_lowerClosure_iff_mem, minimal_mem_upperClosure_iff_mem, disjoint_upperClosure_left, disjoint_upperClosure_right, lowerClosure, disjoint_lowerClosure_left, disjoint_lowerClosure_right, upperClosure, Iic_sup_erase, coe_erase, coe_sdiff, erase_eq, erase_idem, erase_le, erase_lt, erase_sup_Iic, iSup_Iic, lowerClosure, lowerClosure_sup_sdiff, sdiff_eq_left, sdiff_idem, sdiff_le_left, sdiff_lt_left, sdiff_singleton, sdiff_sup_lowerClosure, upperClosure_inter_lowerClosure, Ici_inf_erase, coe_erase, coe_sdiff, erase_eq, erase_idem, erase_inf_Ici, iInf_Ici, le_erase, le_sdiff_left, lt_erase, lt_sdiff_left, sdiff_eq_left, sdiff_idem, sdiff_inf_upperClosure, sdiff_singleton, upperClosure, upperClosure_inf_sdiff, bddAbove_lowerClosure, bddBelow_upperClosure, coe_lowerClosure, coe_upperClosure, gc_lowerClosure_coe, gc_upperClosure_coe, le_upperClosure, lowerBounds_upperClosure, lowerClosure_empty, lowerClosure_eq, lowerClosure_eq_bot_iff, lowerClosure_eq_top, lowerClosure_eq_top_iff, lowerClosure_iUnion, lowerClosure_image, lowerClosure_le, lowerClosure_min, lowerClosure_mono, lowerClosure_sUnion, lowerClosure_singleton, lowerClosure_union, lowerClosure_univ, mem_lowerClosure, mem_upperClosure, ordConnected_iff_upperClosure_inter_lowerClosure, subset_lowerClosure, subset_upperClosure, upperBounds_lowerClosure, upperClosure_anti, upperClosure_empty, upperClosure_eq, upperClosure_eq_bot, upperClosure_eq_bot_iff, upperClosure_eq_top_iff, upperClosure_iUnion, upperClosure_image, upperClosure_min, upperClosure_sUnion, upperClosure_singleton, upperClosure_union, upperClosure_univ | 88 |