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 )
( (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