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 object ; :: 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:24;
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 object ; :: 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:24;
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: (c `) ` = c ;
A17: { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than a ` by A1, Th24;
A18: 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 )
A19: (d `) ` = d ;
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 A19, Th24;
hence a ` [= d by A2, A19, LATTICES:26; :: thesis: verum
end;
A20: { ((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;
A21: 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 )
A22: (d `) ` = d ;
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, A22, Th24;
hence c ` [= d by A4, A22, LATTICES:26; :: thesis: verum
end;
BooleLatt X is \/-distributive by Th26;
then A23: (b `) "/\" (a `) [= c ` by A17, A18, A20, A21;
((b `) "/\" (a `)) ` = ((b `) `) "\/" ((a `) `) by LATTICES:23;
hence c [= b "\/" a by A16, A23, LATTICES:26; :: thesis: verum