let Q be Quantale; :: thesis: for a, b, c being Element of Q holds
( a [*] b [= c iff b [= a -l> c )
let a, b, c be Element of Q; :: thesis: ( a [*] b [= c iff b [= a -l> c )
set X = { d where d is Element of Q : a [*] d [= c } ;
{ d where d is Element of Q : a [*] d [= c } c= H₁(Q)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of Q : a [*] d [= c } or x in H₁(Q) )
assume x in { d where d is Element of Q : a [*] d [= c } ; :: thesis: x in H₁(Q)
then ex d being Element of Q st
( x = d & a [*] d [= c ) ;
hence x in H₁(Q) ; :: thesis: verum

end;

then reconsider X = { d where d is Element of Q : a [*] d [= c } as Subset of Q ;
thus ( a [*] b [= c implies b [= a -l> c ) :: thesis: ( b [= a -l> c implies a [*] b [= c )

proof

assume a [*] b [= c ; :: thesis: b [= a -l> c
then b in X ;
hence b [= a -l> c by LATTICE3:38; :: thesis: verum

end;

deffunc H₅( Element of Q) -> Element of the carrier of Q = a [*] $1;
defpred S₁[ set ] means $1 in X;
defpred S₂[ Element of Q] means a [*] $1 [= c;
assume b [= a -l> c ; :: thesis: a [*] b [= c
then A1: a [*] b [= a [*] ("\/" X) by Th8;

now :: thesis: for d being Element of Q st d in X holds
a [*] d [= c

let d be Element of Q; :: thesis: ( d in X implies a [*] d [= c )
assume d in X ; :: thesis: a [*] d [= c
then ex d1 being Element of Q st
( d = d1 & a [*] d1 [= c ) ;
hence a [*] d [= c ; :: thesis: verum

end;

then A2: for d being Element of Q holds
( S₁[d] iff S₂[d] ) ;
A3: { H₅(d1) where d1 is Element of Q : S₁[d1] } = { H₅(d2) where d2 is Element of Q : S₂[d2] } from FRAENKEL:sch 3(A2);
A4: { (a [*] d) where d is Element of Q : d in X } is_less_than c

proof

let d1 be Element of Q; :: according to LATTICE3:def 17 :: thesis: ( not d1 in { (a [*] d) where d is Element of Q : d in X } or d1 [= c )
assume d1 in { (a [*] d) where d is Element of Q : d in X } ; :: thesis: d1 [= c
then ex d2 being Element of Q st
( d1 = a [*] d2 & a [*] d2 [= c ) by A3;
hence d1 [= c ; :: thesis: verum

end;

a [*] ("\/" X) = "\/" ( { (a [*] d) where d is Element of Q : d in X } ,Q) by Def5;
then a [*] ("\/" X) [= c by A4, LATTICE3:def 21;
hence a [*] b [= c by A1, LATTICES:7; :: thesis: verum