let X be set ; :: thesis: BooleLatt X is /\-distributive
let x be set ; :: according to LATTICE3:def 20 :: thesis: for a, b, c being Element of (BooleLatt X) st x is_greater_than a & ( for d being Element of (BooleLatt X) st x is_greater_than d holds
d [= a ) & { (b "\/" a') where a' is Element of (BooleLatt X) : a' in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a') where a' is Element of (BooleLatt X) : a' in x } is_greater_than d holds
d [= c ) holds
c [= b "\/" a
set B = BooleLatt X;
let a, b, c be Element of (BooleLatt X); :: thesis: ( x is_greater_than a & ( for d being Element of (BooleLatt X) st x is_greater_than d holds
d [= a ) & { (b "\/" a') where a' is Element of (BooleLatt X) : a' in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a') where a' is Element of (BooleLatt X) : a' in x } is_greater_than d holds
d [= c ) implies c [= b "\/" a )
assume that
A1: x is_greater_than a and
A2: for d being Element of (BooleLatt X) st x is_greater_than d holds
d [= a and
A3: { (b "\/" a') where a' is Element of (BooleLatt X) : a' in x } is_greater_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_greater_than d holds
d [= c ; :: thesis: c [= b "\/" a
set x' = { (e ` ) where e is Element of (BooleLatt X) : e in x } ;
set y = { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ;
set y' = { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ;
set z = { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } ;
A5: { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } = { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } }

proof

thus { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } c= { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } :: according to XBOOLE_0:def 10 :: thesis: { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } c= { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } }

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } or s in { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } )
assume s in { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } ; :: thesis: s in { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } }
then consider e being Element of (BooleLatt X) such that
A6: ( s = (b ` ) "/\" e & e in { (e ` ) where e is Element of (BooleLatt X) : e in x } ) ;
consider i being Element of (BooleLatt X) such that
A7: ( e = i ` & i in x ) by A6;
( b "\/" i in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } & (b "\/" i) ` = s ) by A6, A7, LATTICES:51;
hence s in { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ; :: thesis: verum

end;

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } or s in { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } )
assume s in { (e ` ) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ; :: thesis: s in { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } }
then consider e being Element of (BooleLatt X) such that
A8: ( s = e ` & e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ) ;
consider i being Element of (BooleLatt X) such that
A9: ( e = b "\/" i & i in x ) by A8;
( i ` in { (e ` ) where e is Element of (BooleLatt X) : e in x } & s = (b ` ) "/\" (i ` ) ) by A8, A9, LATTICES:51;
hence s in { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } ; :: thesis: verum

end;

A10: ( (a ` ) ` = a & (b ` ) ` = b & (c ` ) ` = c ) by LATTICES:49;
A11: { (e ` ) where e is Element of (BooleLatt X) : e in x } is_less_than a ` by A1, Th24;
A12: for d being Element of (BooleLatt X) st { (e ` ) where e is Element of (BooleLatt X) : e in x } is_less_than d holds
a ` [= d

proof

let d be Element of (BooleLatt X); :: thesis: ( { (e ` ) where e is Element of (BooleLatt X) : e in x } is_less_than d implies a ` [= d )
A13: (d ` ) ` = d by LATTICES:49;
assume { (e ` ) where e is Element of (BooleLatt X) : e in x } is_less_than d ; :: thesis: a ` [= d
then x is_greater_than d ` by A13, Th24;
hence a ` [= d by A2, A13, LATTICES:53; :: thesis: verum

end;

A14: { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } is_less_than c ` by A3, A5, Th24;
A15: for d being Element of (BooleLatt X) st { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } is_less_than d holds
c ` [= d

proof

let d be Element of (BooleLatt X); :: thesis: ( { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } is_less_than d implies c ` [= d )
A16: (d ` ) ` = d by LATTICES:49;
assume { ((b ` ) "/\" e) where e is Element of (BooleLatt X) : e in { (e ` ) where e is Element of (BooleLatt X) : e in x } } is_less_than d ; :: thesis: c ` [= d
then { (b "\/" e) where e is Element of (BooleLatt X) : e in x } is_greater_than d ` by A5, A16, Th24;
hence c ` [= d by A4, A16, LATTICES:53; :: thesis: verum

end;

BooleLatt X is \/-distributive by Th26;
then ( (b ` ) "/\" (a ` ) [= c ` & ((b ` ) "/\" (a ` )) ` = ((b ` ) ` ) "\/" ((a ` ) ` ) ) by A11, A12, A14, A15, Def19, LATTICES:50;
hence c [= b "\/" a by A10, LATTICES:53; :: thesis: verum