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: H₁( 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 set ; :: 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 (x /\ (bool X)) c= union (bool X) by XBOOLE_1:17, ZFMISC_1:95;
A8: union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= union (bool X) by A6, ZFMISC_1:95;
union (bool X) = X by ZFMISC_1:99;
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, A8, Def1;

now

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

end;

then A11: p c= a by ZFMISC_1:94;
A12: 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;

A13: p [= a by A11, Th2;
a [= p by A2, A12;
then A14: a = p by A13, LATTICES:26;

now

let y be set ; :: thesis: ( y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } implies y c= c )
assume A15: 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
A16: y = b "/\" a9 and
a9 in x ;
b "/\" a9 [= c by A3, A15, A16, Def17;
hence y c= c by A16, Th2; :: thesis: verum

end;

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

proof

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

end;

A19: q [= c by A17, Th2;
c [= q by A4, A18;
then A20: c = q by A19, 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 A21: z in b /\ a ; :: thesis: z in c
then A22: z in b by XBOOLE_0:def 4;
z in a by A21, XBOOLE_0:def 4;
then consider y being set such that
A23: z in y and
A24: y in x /\ (bool X) by A14, TARSKI:def 4;
A25: y in x by A24, XBOOLE_0:def 4;
reconsider y = y as Element of (BooleLatt X) by A5, A24, XBOOLE_0:def 4;
A26: b "/\" y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } by A25;
z in b /\ y by A22, A23, XBOOLE_0:def 4;
hence z in c by A20, A26, TARSKI:def 4; :: thesis: verum

end;

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