let Q be Quantale; :: thesis: for a, b, c being Element of Q holds
( a [*] b [= c iff a [= b -r> c )

let a, b, c be Element of Q; :: thesis: ( a [*] b [= c iff a [= b -r> c )
set X = { d where d is Element of Q : d [*] b [= c } ;
{ d where d is Element of Q : d [*] b [= c } c= H1(Q)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of Q : d [*] b [= c } or x in H1(Q) )
assume x in { d where d is Element of Q : d [*] b [= c } ; :: thesis: x in H1(Q)
then ex d being Element of Q st
( x = d & d [*] b [= c ) ;
hence x in H1(Q) ; :: thesis: verum
end;
then reconsider X = { d where d is Element of Q : d [*] b [= c } as Subset of Q ;
thus ( a [*] b [= c implies a [= b -r> c ) :: thesis: ( a [= b -r> c implies a [*] b [= c )
proof
assume a [*] b [= c ; :: thesis: a [= b -r> c
then a in X ;
hence a [= b -r> c by LATTICE3:38; :: thesis: verum
end;
deffunc H5( Element of Q) -> Element of the carrier of Q = \$1 [*] b;
defpred S1[ set ] means \$1 in X;
defpred S2[ Element of Q] means \$1 [*] b [= c;
assume a [= b -r> c ; :: thesis: a [*] b [= c
then A1: a [*] b [= ("\/" X) [*] b by Th8;
now :: thesis: for d being Element of Q st d in X holds
d [*] b [= c
let d be Element of Q; :: thesis: ( d in X implies d [*] b [= c )
assume d in X ; :: thesis: d [*] b [= c
then ex d1 being Element of Q st
( d = d1 & d1 [*] b [= c ) ;
hence d [*] b [= c ; :: thesis: verum
end;
then A2: for d being Element of Q holds
( S1[d] iff S2[d] ) ;
A3: { H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from A4: { (d [*] b) 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 { (d [*] b) where d is Element of Q : d in X } or d1 [= c )
assume d1 in { (d [*] b) where d is Element of Q : d in X } ; :: thesis: d1 [= c
then ex d2 being Element of Q st
( d1 = d2 [*] b & d2 [*] b [= c ) by A3;
hence d1 [= c ; :: thesis: verum
end;
("\/" X) [*] b = "\/" ( { (d [*] b) where d is Element of Q : d in X } ,Q) by Def6;
then ("\/" X) [*] b [= c by ;
hence a [*] b [= c by ; :: thesis: verum