let Q be Girard-Quantale; :: thesis: for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
let X be set ; :: thesis: Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
X is_greater_than "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) 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 "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c )
assume c in X ; :: thesis: "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c
then Bottom c in { (Bottom b) where b is Element of Q : b in X } ;
then A1: Bottom (Bottom c) in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ;
Bottom (Bottom c) = c by Th22;
hence "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c by A1, LATTICE3:38; :: thesis: verum
end;
then A2: "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) 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 { (Bottom b) 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 { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } or x in X )
assume x in { (Bottom a) where a is Element of Q : a in { (Bottom b) 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 { (Bottom b) 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 A3, Th22; :: thesis: verum
end;
then "/\" (X,Q) [= "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) by LATTICE3:45;
then "/\" (X,Q) = "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) by A2, LATTICES:8;
hence Bottom ("/\" (X,Q)) = Bottom (Bottom ("\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q))) by Th24
.= "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by Th22 ;
:: thesis: verum