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 "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 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 "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 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 "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_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_greater_than d holds
d [= c ; :: thesis: c [= b "\/" a
set x9 = { (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 y9 = { (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 and
A7: e in { (e ` ) where e is Element of (BooleLatt X) : e in x } ;
consider i being Element of (BooleLatt X) such that
A8: e = i ` and
A9: i in x by A7;
A10: b "\/" i in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } by A9;
(b "\/" i) ` = s by A6, A8, 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 } } by A10; :: 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
A11: s = e ` and
A12: e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ;
consider i being Element of (BooleLatt X) such that
A13: e = b "\/" i and
A14: i in x by A12;
A15: i ` in { (e ` ) where e is Element of (BooleLatt X) : e in x } by A14;
s = (b ` ) "/\" (i ` ) by A11, A13, 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 } } by A15; :: thesis: verum

end;

A16: (a ` ) ` = a by LATTICES:49;
A17: (b ` ) ` = b by LATTICES:49;
A18: (c ` ) ` = c by LATTICES:49;
A19: { (e ` ) where e is Element of (BooleLatt X) : e in x } is_less_than a ` by A1, Th24;
A20: 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 )
A21: (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 A21, Th24;
hence a ` [= d by A2, A21, LATTICES:53; :: thesis: verum

end;

A22: { ((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;
A23: 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 )
A24: (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, A24, Th24;
hence c ` [= d by A4, A24, LATTICES:53; :: thesis: verum

end;

BooleLatt X is \/-distributive by Th26;
then A25: (b ` ) "/\" (a ` ) [= c ` by A19, A20, A22, A23, Def19;
((b ` ) "/\" (a ` )) ` = ((b ` ) ` ) "\/" ((a ` ) ` ) by LATTICES:50;
hence c [= b "\/" a by A16, A17, A18, A25, LATTICES:53; :: thesis: verum