environ
vocabularies HIDDEN, WAYBEL_0, SUBSET_1, XBOOLE_0, ORDERS_2, FUNCT_1, RELAT_1, TARSKI, NUMBERS, FUNCT_7, TREES_2, RELAT_2, XXREAL_0, STRUCT_0, ORDINAL2, LATTICES, ORDERS_1, ZFMISC_1, YELLOW_0, EQREL_1, REWRITE1, FUNCOP_1, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, CARD_FIL, SETFAM_1, ARYTM_3, CARD_1, NAT_1, ORDINAL1, YELLOW_8, FINSET_1, INT_2, YELLOW_1, FUNCT_3, LATTICE2, ARYTM_0, WAYBEL_5, PBOOLE, YELLOW_2, FUNCT_6, CARD_3, WAYBEL_6;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FINSET_1, RELAT_1, RELAT_2, ORDERS_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, STRUCT_0, ORDERS_2, CARD_3, LATTICE3, FUNCT_3, FUNCT_6, PBOOLE, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1, YELLOW_2, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, YELLOW_7, FUNCT_7, ABIAN, XXREAL_0;
definitions TARSKI, RELAT_2, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_5, FUNCT_1, ORDERS_3, XBOOLE_0;
theorems WAYBEL_3, TARSKI, YELLOW_0, ZFMISC_1, WAYBEL_0, ORDERS_2, WAYBEL_4, FUNCT_2, FUNCT_1, LATTICE3, NAT_1, WAYBEL_1, YELLOW_1, YELLOW_5, WAYBEL_2, YELLOW_2, WAYBEL_5, CARD_3, FUNCT_6, YELLOW_7, ORDERS_1, FUNCT_3, YELLOW_4, YELLOW_3, FUNCOP_1, RELAT_1, RELSET_1, ORDINAL1, XBOOLE_0, XBOOLE_1, FUNCT_7, CARD_1, PARTFUN1;
schemes FUNCT_1, FINSET_1, CLASSES1, NAT_1, FUNCT_2, YELLOW_3, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCOP_1, FINSET_1, PBOOLE, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_7, ORDINAL1, RELSET_1, XXREAL_0, CARD_1, RELAT_1, XCMPLX_0, NAT_1, FUNCT_7;
constructors HIDDEN, SETFAM_1, XXREAL_0, NAT_1, FUNCT_7, BORSUK_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, RELSET_1, NUMBERS, ABIAN;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RELAT_1, LATTICE3, WAYBEL_0, SUBSET_1, STRUCT_0, ORDINAL1;
expansions TARSKI, RELAT_2, LATTICE3, WAYBEL_0, WAYBEL_1, XBOOLE_0, ORDINAL1;
Lm1:
for S, T being non empty with_suprema Poset
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
Lm2:
for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
L is completely-distributive
Lm3:
for L being complete completely-distributive LATTICE holds
( L is distributive & L is continuous & L ~ is continuous )
Lm4:
for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds
for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )