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 "/\" a') where a' is Element of (BooleLatt X) : a' in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a') where a' is Element of (BooleLatt X) : a' 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 "/\" a') where a' is Element of (BooleLatt X) : a' in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a') where a' is Element of (BooleLatt X) : a' 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 "/\" a') where a' is Element of (BooleLatt X) : a' in x } is_less_than c and
A4: for d being Element of (BooleLatt X) st { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } is_less_than d holds
c [= d ; :: thesis: b "/\" a [= c
set Y = { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } ;
A5: H₁( BooleLatt X) = bool X by Def1;
A6: { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } c= bool X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } or z in bool X )
assume z in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } ; :: thesis: z in bool X
then ex a' being Element of (BooleLatt X) st
( z = b "/\" a' & a' in x ) ;
hence z in bool X by A5; :: thesis: verum

end;

x /\ (bool X) c= bool X by XBOOLE_1:17;
then ( union (x /\ (bool X)) c= union (bool X) & union { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } c= union (bool X) & union (bool X) = X ) by A6, ZFMISC_1:95, ZFMISC_1:99;
then reconsider p = union (x /\ (bool X)), q = union { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } as Element of (BooleLatt X) by Def1;

now

let y be set ; :: thesis: ( y in x /\ (bool X) implies y c= a )
assume A7: y in x /\ (bool X) ; :: thesis: y c= a
then A8: ( y in x & y in bool X ) by XBOOLE_0:def 4;
reconsider y' = y as Element of (BooleLatt X) by A5, A7, XBOOLE_0:def 4;
y' [= a by A1, A8, Def17;
hence y c= a by Th2; :: thesis: verum

end;

then A9: p c= a by ZFMISC_1:94;
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:92;
hence q [= p by Th2; :: thesis: verum

end;

then ( p [= a & a [= p ) by A2, A9, Th2;
then A10: a = p by LATTICES:26;

now

let y be set ; :: thesis: ( y in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } implies y c= c )
assume A11: y in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } ; :: thesis: y c= c
then consider a' being Element of (BooleLatt X) such that
A12: ( y = b "/\" a' & a' in x ) ;
b "/\" a' [= c by A3, A11, A12, Def17;
hence y c= c by A12, Th2; :: thesis: verum

end;

then A13: q c= c by ZFMISC_1:94;
{ (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } is_less_than q

proof

let p be Element of (BooleLatt X); :: according to LATTICE3:def 17 :: thesis: ( p in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } implies p [= q )
assume p in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } ; :: thesis: p [= q
then p c= q by ZFMISC_1:92;
hence p [= q by Th2; :: thesis: verum

end;

then ( q [= c & c [= q ) by A4, A13, Th2;
then A14: ( c = q & b /\ a = b "/\" a ) by LATTICES:26;
b /\ a c= c

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in b /\ a or z in c )
assume z in b /\ a ; :: thesis: z in c
then A15: ( z in b & z in a ) by XBOOLE_0:def 4;
then consider y being set such that
A16: ( z in y & y in x /\ (bool X) ) by A10, TARSKI:def 4;
A17: ( y in x & y in bool X ) by A16, XBOOLE_0:def 4;
reconsider y = y as Element of (BooleLatt X) by A5, A16, XBOOLE_0:def 4;
( b "/\" y in { (b "/\" a') where a' is Element of (BooleLatt X) : a' in x } & b "/\" y = b /\ y & z in b /\ y ) by A15, A16, A17, XBOOLE_0:def 4;
hence z in c by A14, TARSKI:def 4; :: thesis: verum

end;

hence b "/\" a [= c by Th2; :: thesis: verum