let Q be Girard-Quantale; :: thesis: for a1, a2, b1, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds
a1 delta a2 [= b1 delta b2
let a1, a2, b1, b2 be Element of Q; :: thesis: ( a1 [= b1 & a2 [= b2 implies a1 delta a2 [= b1 delta b2 )
assume ( a1 [= b1 & a2 [= b2 ) ; :: thesis: a1 delta a2 [= b1 delta b2
then ( Bottom b1 [= Bottom a1 & Bottom b2 [= Bottom a2 ) by Th13;
then (Bottom b1) [*] (Bottom b2) [= (Bottom a1) [*] (Bottom a2) by Th9;
hence a1 delta a2 [= b1 delta b2 by Th13; :: thesis: verum