let Q be Girard-Quantale; :: thesis: for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { () where a is Element of Q : a in X } ,Q)
let X be set ; :: thesis: Bottom ("/\" (X,Q)) = "\/" ( { () where a is Element of Q : a in X } ,Q)
X is_greater_than "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q)
proof
let c be Element of Q; :: according to LATTICE3:def 16 :: thesis: ( not c in X or "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q) [= c )
assume c in X ; :: thesis: "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q) [= c
then Bottom c in { () where b is Element of Q : b in X } ;
then A1: Bottom () in { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ;
Bottom () = c by Th22;
hence "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q) [= c by ; :: thesis: verum
end;
then A2: "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q) [= "/\" (X,Q) by LATTICE3:39;
{ (Bottom a) where a is Element of Q : a in { () where b is Element of Q : b in X } } c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { () where a is Element of Q : a in { () where b is Element of Q : b in X } } or x in X )
assume x in { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ; :: thesis: x in X
then consider a being Element of Q such that
A3: ( x = Bottom a & a in { () where b is Element of Q : b in X } ) ;
ex b being Element of Q st
( a = Bottom b & b in X ) by A3;
hence x in X by ; :: thesis: verum
end;
then "/\" (X,Q) [= "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q) by LATTICE3:45;
then "/\" (X,Q) = "/\" ( { () where a is Element of Q : a in { () where b is Element of Q : b in X } } ,Q) by ;
hence Bottom ("/\" (X,Q)) = Bottom (Bottom ("\/" ( { () where a is Element of Q : a in X } ,Q))) by Th24
.= "\/" ( { () where a is Element of Q : a in X } ,Q) by Th22 ;
:: thesis: verum