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)

{ (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } c= X

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

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

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;
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;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

{ (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } c= X

proof

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;
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;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

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