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 }

{ d where d is Element of Q : b [*] d [= s } c= { c where c is Element of Q : a [*] c [= s }

( 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

hence
b -r> s [= a -r> s
by LATTICE3:45; :: thesis: b -l> s [= a -l> s
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;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

{ d where d is Element of Q : b [*] d [= s } c= { c where c is Element of Q : a [*] c [= s }

proof

hence
b -l> s [= a -l> s
by LATTICE3:45; :: thesis: verum
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;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