let Q be Girard-Quantale; :: thesis: for a being Element of Q holds
( a delta (Bottom Q) = a & (Bottom Q) delta a = a )
let a be Element of Q; :: thesis: ( a delta (Bottom Q) = a & (Bottom Q) delta a = a )
( a delta (Bottom Q) = Bottom ((Bottom a) [*] (Bottom (Bottom Q))) & (Bottom Q) delta a = Bottom ((Bottom (Bottom Q)) [*] (Bottom a)) & Bottom (Bottom Q) = (Bottom Q) -r> (Bottom Q) & Top Q = (Bottom Q) -r> (Bottom Q) & (Bottom a) [*] (Top Q) = Bottom a & (Top Q) [*] (Bottom a) = Bottom a ) by Th32;
hence ( a delta (Bottom Q) = a & (Bottom Q) delta a = a ) by Th22; :: thesis: verum