environ
vocabularies HIDDEN, FINSET_1, LATTICES, LATTICE3, XBOOLE_0, STRUCT_0, ZFMISC_1, SUBSET_1, XXREAL_0, NUMBERS, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, FUNCT_1, TARSKI, ORDERS_2, FILTER_1, EQREL_1, PBOOLE, REWRITE1, WELLORD1, WAYBEL_6, RELAT_2, ZF_LANG, BINOP_1, LATTICE6, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, BINOP_1, FINSET_1, WELLORD1, WAYBEL_6, STRUCT_0, LATTICES, LATTICE3, ORDERS_2, FINSEQ_1, WELLFND1, YELLOW_0, LATTICE2;
definitions TARSKI, WELLFND1, WELLORD1;
theorems TARSKI, FUNCT_1, LATTICES, LATTICE3, ORDERS_2, VECTSP_8, FINSEQ_1, WAYBEL_6, NAT_1, INT_1, RELAT_1, YELLOW_0, WELLORD1, XBOOLE_0, XXREAL_0, STRUCT_0, CARD_1, ZFMISC_1;
schemes NAT_1, WELLFND1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, INT_1, FINSEQ_1, FINSEQ_6, STRUCT_0, LATTICES, ORDERS_2, LATTICE2, LATTICE3, WAYBEL_0, KNASTER, YELLOW_1, ORDINAL1, CARD_1;
constructors HIDDEN, WELLORD1, BINOP_1, REAL_1, REALSET2, LATTICE2, WAYBEL_0, WAYBEL_6, WELLFND1, RELSET_1, LATTICE3;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI, WELLFND1, WELLORD1;
Lm1:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
Lm2:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
Lm3:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
Lm4:
for L being finite Lattice ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a
Lm5:
for L being finite Lattice holds L is complete
Lm6:
for L being finite Lattice holds (LattPOSet L) ~ is well_founded
Lm7:
for L being finite Lattice holds
( L is noetherian & L is co-noetherian )
by Lm6;
Lm8:
for L being Lattice
for a, b being Element of L holds
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
Lm9:
for L being complete co-noetherian Lattice holds MIRRS L is infimum-dense
Lm10:
for L being complete noetherian Lattice holds JIRRS L is supremum-dense