environ
vocabularies HIDDEN, XBOOLE_0, RELAT_2, ORDERS_2, SUBSET_1, XXREAL_0, WAYBEL_8, TARSKI, RCOMP_1, STRUCT_0, YELLOW_0, LATTICE3, CARD_FIL, LATTICES, WAYBEL_0, WAYBEL_5, GROUP_6, WAYBEL10, YELLOW_1, FINSET_1, SETFAM_1, REWRITE1, RELAT_1, FUNCT_1, ZFMISC_1, CAT_1, EQREL_1, WELLORD2, ORDINAL2, WAYBEL_3, SEQM_3, PBOOLE, CARD_3, WELLORD1, WAYBEL_1, YELLOW_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, RELAT_1, ORDERS_1, ORDERS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, PBOOLE, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10;
definitions TARSKI;
theorems TARSKI, ZFMISC_1, SETFAM_1, ORDERS_2, FUNCT_1, FUNCT_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, CARD_3, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_5, WAYBEL_8, WAYBEL10, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, PARTFUN1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL10;
constructors HIDDEN, DOMAIN_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL10, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities YELLOW_2, STRUCT_0;
expansions TARSKI;
Lm1:
for L being lower-bounded LATTICE st L is algebraic holds
ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
Lm2:
for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
Lm3:
for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
Lm4:
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 st x << y holds
f . x << f . y
Lm5:
for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) holds
L is algebraic