let Q be Quantale; :: thesis: for s, a, b being Element of Q st a [= b holds
( b -r> s [= a -r> s & b -l> s [= a -l> s )

let s, a, b be Element of Q; :: thesis: ( a [= b implies ( b -r> s [= a -r> s & b -l> s [= a -l> s ) )
assume A1: a [= b ; :: thesis: ( b -r> s [= a -r> s & b -l> s [= a -l> s )
{ d where d is Element of Q : d [*] b [= s } c= { c where c is Element of Q : c [*] a [= s }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of Q : d [*] b [= s } or x in { c where c is Element of Q : c [*] a [= s } )
assume x in { d where d is Element of Q : d [*] b [= s } ; :: thesis: x in { c where c is Element of Q : c [*] a [= s }
then consider d being Element of Q such that
A2: x = d and
A3: d [*] b [= s ;
d [*] a [= d [*] b by ;
then d [*] a [= s by ;
hence x in { c where c is Element of Q : c [*] a [= s } by A2; :: thesis: verum
end;
hence b -r> s [= a -r> s by LATTICE3:45; :: thesis: b -l> s [= a -l> s
{ d where d is Element of Q : b [*] d [= s } c= { c where c is Element of Q : a [*] c [= s }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of Q : b [*] d [= s } or x in { c where c is Element of Q : a [*] c [= s } )
assume x in { d where d is Element of Q : b [*] d [= s } ; :: thesis: x in { c where c is Element of Q : a [*] c [= s }
then consider d being Element of Q such that
A4: x = d and
A5: b [*] d [= s ;
a [*] d [= b [*] d by ;
then a [*] d [= s by ;
hence x in { c where c is Element of Q : a [*] c [= s } by A4; :: thesis: verum
end;
hence b -l> s [= a -l> s by LATTICE3:45; :: thesis: verum