let Q be Girard-Quantale; :: thesis: for a, b, c being Element of Q holds
( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )
let a, b, c be Element of Q; :: thesis: ( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )
thus a delta (b "/\" c) = Bottom ((Bottom a) [*] ((Bottom b) "\/" (Bottom c))) by Th26
.= Bottom (((Bottom a) [*] (Bottom b)) "\/" ((Bottom a) [*] (Bottom c))) by Th6
.= (a delta b) "/\" (a delta c) by Th26 ; :: thesis: (b "/\" c) delta a = (b delta a) "/\" (c delta a)
thus (b "/\" c) delta a = Bottom (((Bottom b) "\/" (Bottom c)) [*] (Bottom a)) by Th26
.= Bottom (((Bottom b) [*] (Bottom a)) "\/" ((Bottom c) [*] (Bottom a))) by Th6
.= (b delta a) "/\" (c delta a) by Th26 ; :: thesis: verum