let Q be Quantale; :: thesis: for a, b, c being Element of Q st a [= b holds
( a [*] c [= b [*] c & c [*] a [= c [*] b )
let a, b, c be Element of Q; :: thesis: ( a [= b implies ( a [*] c [= b [*] c & c [*] a [= c [*] b ) )
assume A1: a [= b ; :: thesis: ( a [*] c [= b [*] c & c [*] a [= c [*] b )
thus (a [*] c) "\/" (b [*] c) = (a "\/" b) [*] c by Th6
.= b [*] c by A1, LATTICES:def 3 ; :: according to LATTICES:def 3 :: thesis: c [*] a [= c [*] b
thus (c [*] a) "\/" (c [*] b) = c [*] (a "\/" b) by Th6
.= c [*] b by A1, LATTICES:def 3 ; :: according to LATTICES:def 3 :: thesis: verum