let Q be Quantale; :: thesis: for a, b, c, d being Element of Q st a [= b & c [= d holds
a [*] c [= b [*] d
let a, b, c, d be Element of Q; :: thesis: ( a [= b & c [= d implies a [*] c [= b [*] d )
assume ( a [= b & c [= d ) ; :: thesis: a [*] c [= b [*] d
then ( a [*] c [= b [*] c & b [*] c [= b [*] d ) by Th8;
hence a [*] c [= b [*] d by LATTICES:7; :: thesis: verum