let Q be Girard-Quantale; :: thesis: for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c)
let a, b, c be Element of Q; :: thesis: (a delta b) delta c = a delta (b delta c)
thus (a delta b) delta c = Bottom (((Bottom a) [*] (Bottom b)) [*] (Bottom c)) by Th22
.= Bottom ((Bottom a) [*] ((Bottom b) [*] (Bottom c))) by GROUP_1:def 3
.= a delta (b delta c) by Th22 ; :: thesis: verum