let Q be Girard-Quantale; :: thesis: for a, b being Element of Q holds
( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )
let a, b be Element of Q; :: thesis: ( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )
A1: { (Bottom c) where c is Element of Q : c in {a,b} } = {(Bottom a),(Bottom b)}
proof
thus { (Bottom c) where c is Element of Q : c in {a,b} } c= {(Bottom a),(Bottom b)} :: according to XBOOLE_0:def 10 :: thesis: {(Bottom a),(Bottom b)} c= { (Bottom c) where c is Element of Q : c in {a,b} }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Bottom c) where c is Element of Q : c in {a,b} } or x in {(Bottom a),(Bottom b)} )
assume x in { (Bottom c) where c is Element of Q : c in {a,b} } ; :: thesis: x in {(Bottom a),(Bottom b)}
then consider c being Element of Q such that
A2: x = Bottom c and
A3: c in {a,b} ;
( c = a or c = b ) by A3, TARSKI:def 2;
hence x in {(Bottom a),(Bottom b)} by A2, TARSKI:def 2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Bottom a),(Bottom b)} or x in { (Bottom c) where c is Element of Q : c in {a,b} } )
assume x in {(Bottom a),(Bottom b)} ; :: thesis: x in { (Bottom c) where c is Element of Q : c in {a,b} }
then ( ( x = Bottom a & a in {a,b} ) or ( x = Bottom b & b in {a,b} ) ) by TARSKI:def 2;
hence x in { (Bottom c) where c is Element of Q : c in {a,b} } ; :: thesis: verum
end;
( a "\/" b = "\/" {a,b} & (Bottom a) "/\" (Bottom b) = "/\" {(Bottom a),(Bottom b)} ) by LATTICE3:43;
hence Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) by A1, Th24; :: thesis: Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b)
( (Bottom a) "\/" (Bottom b) = "\/" {(Bottom a),(Bottom b)} & a "/\" b = "/\" {a,b} ) by LATTICE3:43;
hence Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) by A1, Th25; :: thesis: verum