begin
theorem
canceled;
theorem
canceled;
theorem
for
X being
set st
X <> {} & ( for
Z being
set st
Z <> {} &
Z c= X &
Z is
c=-linear holds
ex
Y being
set st
(
Y in X & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) ) ) holds
ex
Y being
set st
(
Y in X & ( for
Z being
set st
Z in X &
Z <> Y holds
not
Y c= Z ) )
begin
theorem
theorem
theorem
:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem LATTICE4:def 2 :
canceled;
:: deftheorem LATTICE4:def 3 :
canceled;
:: deftheorem LATTICE4:def 4 :
canceled;
:: deftheorem defines are_isomorphic LATTICE4:def 5 :
:: deftheorem Def6 defines preserves_implication LATTICE4:def 6 :
:: deftheorem Def7 defines preserves_top LATTICE4:def 7 :
:: deftheorem Def8 defines preserves_bottom LATTICE4:def 8 :
:: deftheorem Def9 defines preserves_complement LATTICE4:def 9 :
:: deftheorem LATTICE4:def 10 :
canceled;
theorem Th10:
theorem
:: deftheorem LATTICE4:def 11 :
canceled;
:: deftheorem defines FinJoin LATTICE4:def 12 :
:: deftheorem defines FinMeet LATTICE4:def 13 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem Th17:
begin
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem Th21:
theorem
Lm1:
for 0L being lower-bounded Lattice
for f being Function of the carrier of 0L,the carrier of 0L holds FinJoin ({}. the carrier of 0L),f = Bottom 0L
theorem
theorem Th24:
begin
theorem Th25:
Lm2:
for 1L being upper-bounded Lattice
for f being Function of the carrier of 1L,the carrier of 1L holds FinMeet ({}. the carrier of 1L),f = Top 1L
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
begin
Lm3:
for DL being distributive upper-bounded Lattice
for B being Finite_Subset of the carrier of DL
for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)
theorem Th32:
begin
theorem Th33:
theorem Th34:
theorem
begin
theorem Th36:
theorem Th37:
theorem
:: deftheorem Def14 defines Field LATTICE4:def 14 :
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
:: deftheorem Def15 defines field_by LATTICE4:def 15 :
:: deftheorem defines SetImp LATTICE4:def 16 :
theorem
theorem Th44:
:: deftheorem Def17 defines comp LATTICE4:def 17 :
theorem Th45:
theorem
theorem
theorem Th48:
theorem Th49:
theorem