environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, FUNCT_1, NUMBERS, STRUCT_0, SUBSET_1, XXREAL_0, FINSET_1, TARSKI, CARD_1, FINSEQ_1, PRE_TOPC, RCOMP_1, SETFAM_1, TOPS_1, CARD_3, ORDINAL1, RELAT_2, WAYBEL_0, YELLOW_0, ORDINAL2, LATTICE3, LATTICES, EQREL_1, WAYBEL_6, WAYBEL_3, FINSUB_1, CARD_FIL, MSAFREE, RELAT_1, ARYTM_3, YELLOW_8, ORDERS_1, ZFMISC_1, XXREAL_2, YELLOW_1, TOPS_3, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, NAT_1, SETFAM_1, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1, FINSUB_1, DOMAIN_1, XXREAL_0, FUNCT_2, STRUCT_0, CARD_3, PRE_TOPC, ORDERS_2, TOPS_1, TOPS_2, TOPS_3, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8;
definitions TARSKI, WAYBEL_0, PRE_TOPC, TOPS_2, YELLOW_4, WAYBEL_6, YELLOW_8, CARD_3, LATTICE3, XBOOLE_0;
theorems CARD_1, FUNCT_2, LATTICE3, ORDERS_2, TARSKI, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_0, YELLOW_1, YELLOW_3, YELLOW_4, ZFMISC_1, PRE_TOPC, WAYBEL_7, FUNCT_1, TOPS_1, TOPS_3, YELLOW_8, MSSUBFAM, NAT_1, FINSEQ_1, FINSUB_1, RELAT_1, YELLOW_2, SETFAM_1, XBOOLE_0, XBOOLE_1, SUBSET_1, CARD_3, ORDINAL1;
schemes FUNCT_2, TREES_2, SETWISEO, NAT_1, RECDEF_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XREAL_0, CARD_1, FINSEQ_1, STRUCT_0, LATTICE3, YELLOW_0, PRE_TOPC, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_4, WAYBEL_3, YELLOW_6, WAYBEL_6, WAYBEL_7, YELLOW_8, SETWISEO, CARD_3, TOPS_1, RELAT_1, NAT_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, SETWISEO, XXREAL_0, NAT_1, NAT_D, TOPS_1, TOPS_2, TOPS_3, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8, RELSET_1, FINSEQ_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities WAYBEL_0, YELLOW_4, XBOOLE_0, SUBSET_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, PRE_TOPC, TOPS_2, YELLOW_4, WAYBEL_6, YELLOW_8, LATTICE3, XBOOLE_0;
Lm1:
for L being non empty RelStr
for f being sequence of the carrier of L
for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L
Lm2:
for L being non empty RelStr
for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L
Lm3:
for L being Semilattice
for F being Filter of L holds F = uparrow (fininfs F)
by WAYBEL_0:62;
Lm4:
for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F