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)
{ (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } is_less_than Bottom Q
proof
let c be Element of Q; :: according to LATTICE3:def 17 :: thesis: ( not c in { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } or c [= Bottom Q )
assume c in { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } ; :: thesis: c [= Bottom Q
then consider b being Element of Q such that
A1: ( c = ("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b & b in X ) ;
Bottom b in { (Bottom a) where a is Element of Q : a in X } by A1;
then "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) [= Bottom b by LATTICE3:38;
hence c [= Bottom Q by A1, Th12; :: thesis: verum
end;
then "\/" ( { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } ,Q) [= Bottom Q by LATTICE3:def 21;
then ("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] ("\/" (X,Q)) [= Bottom Q by Def5;
then A2: "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) [= Bottom ("\/" (X,Q)) by Th12;
Bottom ("\/" (X,Q)) is_less_than { (Bottom a) where a is Element of Q : a in X }
proof
let b be Element of Q; :: according to LATTICE3:def 16 :: thesis: ( not b in { (Bottom a) where a is Element of Q : a in X } or Bottom ("\/" (X,Q)) [= b )
assume b in { (Bottom a) where a is Element of Q : a in X } ; :: thesis: Bottom ("\/" (X,Q)) [= b
then consider a being Element of Q such that
A3: b = Bottom a and
A4: a in X ;
a [= "\/" (X,Q) by A4, LATTICE3:38;
hence Bottom ("\/" (X,Q)) [= b by A3, Th13; :: thesis: verum
end;
then Bottom ("\/" (X,Q)) [= "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by LATTICE3:39;
hence Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by A2, LATTICES:8; :: thesis: verum