environ
vocabularies HIDDEN, FINSET_1, SETFAM_1, TARSKI, SUBSET_1, XBOOLE_0, NAT_1, CARD_1, ARYTM_3, STRUCT_0, RELAT_2, LATTICE3, ORDERS_2, WAYBEL_0, LATTICES, XXREAL_0, EQREL_1, REWRITE1, ORDINAL2, WAYBEL_3, WAYBEL_6, RELAT_1, INT_2, ZFMISC_1, WAYBEL_8, RCOMP_1, PRE_TOPC, YELLOW_8, YELLOW_1, WAYBEL_9, RLVECT_3, WAYBEL11, PROB_1, YELLOW_6, FUNCT_1, WAYBEL_2, TMAP_1, CONNSP_2, TOPS_1, CARD_FIL, YELLOW_0, WAYBEL_5, ARYTM_0, WAYBEL14;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, NAT_1, SETFAM_1, FINSET_1, DOMAIN_1, FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, ORDERS_2, LATTICE3, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, BORSUK_1, TMAP_1, CANTOR_1, COMPTS_1, YELLOW_0, YELLOW_1, YELLOW_3, YELLOW_4, YELLOW_6, YELLOW_7, YELLOW_8, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8, WAYBEL_9, WAYBEL11;
definitions TARSKI, WAYBEL_0, WAYBEL_6, TMAP_1, YELLOW_8, COMPTS_1, WAYBEL_3, WAYBEL_1, WAYBEL_8, TOPS_2, XBOOLE_0, SETFAM_1;
theorems TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, FUNCT_1, FUNCT_2, SETFAM_1, LATTICE3, CARD_2, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TMAP_1, CONNSP_2, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, YELLOW_6, YELLOW_7, YELLOW_8, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8, WAYBEL11, WAYBEL12, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1;
registrations SUBSET_1, RELSET_1, FINSET_1, XCMPLX_0, STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_4, WAYBEL_3, YELLOW_6, WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL11, ORDINAL1, CARD_1, TOPS_1, NAT_1;
constructors HIDDEN, SETFAM_1, FINSUB_1, NAT_1, TOPS_1, TOPS_2, BORSUK_1, TMAP_1, T_0TOPSP, CANTOR_1, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL11, COMPTS_1, BINOP_1, WAYBEL_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities WAYBEL_0, WAYBEL_3, WAYBEL_8, XBOOLE_0, SUBSET_1, BINOP_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, WAYBEL_6, COMPTS_1, WAYBEL_3, TOPS_2, XBOOLE_0;
Lm1:
for S being 1-sorted
for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )
Lm2:
for L being complete Scott TopLattice
for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed