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 A1, Th8;
then d [*] a [= s by A3, LATTICES:7;
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 A1, Th8;
then a [*] d [= s by A5, LATTICES:7;
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