environ
vocabularies HIDDEN, NUMBERS, CARD_1, XBOOLE_0, TARSKI, RELAT_2, LATTICE3, ORDERS_2, SUBSET_1, LATTICES, EQREL_1, XXREAL_0, WAYBEL_0, YELLOW_1, STRUCT_0, CAT_1, LATTICE5, WELLORD1, FUNCT_1, SEQM_3, YELLOW_0, RELAT_1, ORDINAL2, MEASURE5, FINSET_1, ORDERS_1, REWRITE1, YELLOW11;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS, ORDERS_1, DOMAIN_1, FINSET_1, STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_1, LATTICE5, WAYBEL_0;
definitions TARSKI, YELLOW_0, WAYBEL_1, FUNCT_1, WAYBEL_0, LATTICE3, XBOOLE_0;
theorems WAYBEL_1, YELLOW_0, YELLOW_3, YELLOW_5, LATTICE3, TARSKI, FUNCT_2, WAYBEL_0, ZFMISC_1, FUNCT_1, ORDERS_2, YELLOW_1, ENUMSET1, CARD_1, FINSET_1, XBOOLE_0, XBOOLE_1, NAT_1;
schemes FUNCT_2, FINSET_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, ORDINAL1;
constructors HIDDEN, DOMAIN_1, XXREAL_0, LATTICE3, ORDERS_3, WAYBEL_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities WAYBEL_0, ORDINAL1, CARD_1;
expansions TARSKI, WAYBEL_1, LATTICE3, XBOOLE_0;
Lm1:
3 \ 2 c= 3 \ 1
Lm2:
for L being LATTICE holds
( L is modular iff for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) )
Lm3:
for L being LATTICE st L is modular holds
( L is distributive iff for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) )