environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, SUBSET_1, WAYBEL_8, WAYBEL_3, STRUCT_0, TARSKI, WAYBEL_0, XXREAL_0, RCOMP_1, RELAT_2, YELLOW_1, CARD_FIL, YELLOW_0, ORDINAL2, LATTICE3, EQREL_1, FINSET_1, CAT_1, REWRITE1, LATTICES, PRE_TOPC, CARD_1, SETFAM_1, RLVECT_3, ORDINAL1, XXREAL_2, ZFMISC_1, FUNCT_1, WELLORD2, RELAT_1, SEQM_3, YELLOW_2, WAYBEL_1, WELLORD1, FUNCT_2, WAYBEL23;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, FINSET_1, ORDINAL1, CARD_1, PRE_TOPC, ORDERS_2, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8;
definitions TARSKI, LATTICE3, YELLOW_0, XBOOLE_0;
theorems TARSKI, SETFAM_1, ZFMISC_1, FUNCT_1, FUNCT_2, CANTOR_1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_5, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL10, WAYBEL13, WAYBEL20, WAYBEL21, XBOOLE_0, XBOOLE_1;
schemes ORDINAL1, FUNCT_2, MONOID_1;
registrations RELSET_1, FINSET_1, CARD_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL14, SUBSET_1;
constructors HIDDEN, DOMAIN_1, CANTOR_1, ORDERS_3, WAYBEL_8, RELSET_1, WAYBEL20, TOPS_2;
requirements HIDDEN, SUBSET, BOOLE;
equalities YELLOW_0, XBOOLE_0, STRUCT_0;
expansions TARSKI, LATTICE3, YELLOW_0, XBOOLE_0;
Lm1:
for X being non empty set
for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
Lm2:
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) holds
( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
Lm3:
for L being lower-bounded continuous LATTICE
for B being Subset of L st ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) holds
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
Lm4:
for L being lower-bounded continuous LATTICE st L is algebraic holds
( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )
Lm5:
for L being lower-bounded continuous LATTICE st ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 holds
L is algebraic