let X be set ; :: thesis: BooleLatt X is \/-distributive
let x be set ; :: according to LATTICE3:def 19 :: thesis: for a, b, c being Element of (BooleLatt X) st x is_less_than a & ( for d being Element of (BooleLatt X) st x is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds
c [= d ) holds
b "/\" a [= c
set B = BooleLatt X;
let a, b, c be Element of (BooleLatt X); :: thesis: ( x is_less_than a & ( for d being Element of (BooleLatt X) st x is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds
c [= d ) implies b "/\" a [= c )
assume that
A1: x is_less_than a and
A2: for d being Element of (BooleLatt X) st x is_less_than d holds
a [= d and
A3: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c and
A4: for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds
c [= d ; :: thesis: b "/\" a [= c
set Y = { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ;
A5: H1( BooleLatt X) = bool X by Def1;
A6: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= bool X
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } or z in bool X )
assume z in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; :: thesis: z in bool X
then ex a9 being Element of (BooleLatt X) st
( z = b "/\" a9 & a9 in x ) ;
hence z in bool X by A5; :: thesis: verum
end;
A7: union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= union (bool X) by A6, ZFMISC_1:77;
union (bool X) = X by ZFMISC_1:81;
then reconsider p = union (x /\ (bool X)), q = union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } as Element of (BooleLatt X) by A7, Def1;
now :: thesis: for y being set st y in x /\ (bool X) holds
y c= a
let y be set ; :: thesis: ( y in x /\ (bool X) implies y c= a )
assume A8: y in x /\ (bool X) ; :: thesis: y c= a
then A9: y in x by XBOOLE_0:def 4;
reconsider y9 = y as Element of (BooleLatt X) by A5, A8;
y9 [= a by A1, A9;
hence y c= a by Th2; :: thesis: verum
end;
then A10: p c= a by ZFMISC_1:76;
A11: x is_less_than p
proof
let q be Element of (BooleLatt X); :: according to LATTICE3:def 17 :: thesis: ( q in x implies q [= p )
assume q in x ; :: thesis: q [= p
then q in x /\ (bool X) by A5, XBOOLE_0:def 4;
then q c= p by ZFMISC_1:74;
hence q [= p by Th2; :: thesis: verum
end;
A12: p [= a by A10, Th2;
a [= p by A2, A11;
then A13: a = p by A12;
now :: thesis: for y being set st y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } holds
y c= c
let y be set ; :: thesis: ( y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } implies y c= c )
assume A14: y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; :: thesis: y c= c
then consider a9 being Element of (BooleLatt X) such that
A15: y = b "/\" a9 and
a9 in x ;
b "/\" a9 [= c by A3, A14, A15;
hence y c= c by A15, Th2; :: thesis: verum
end;
then A16: q c= c by ZFMISC_1:76;
A17: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than q by ZFMISC_1:74, Th2;
A18: q [= c by A16, Th2;
c [= q by A4, A17;
then A19: c = q by A18;
b /\ a c= c
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in b /\ a or z in c )
assume A20: z in b /\ a ; :: thesis: z in c
then A21: z in b by XBOOLE_0:def 4;
z in a by A20, XBOOLE_0:def 4;
then consider y being set such that
A22: z in y and
A23: y in x /\ (bool X) by A13, TARSKI:def 4;
A24: y in x by A23, XBOOLE_0:def 4;
reconsider y = y as Element of (BooleLatt X) by A5, A23;
A25: b "/\" y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } by A24;
z in b /\ y by A21, A22, XBOOLE_0:def 4;
hence z in c by A19, A25, TARSKI:def 4; :: thesis: verum
end;
hence b "/\" a [= c by Th2; :: thesis: verum