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= H_{1}(Q)

thus ( a [*] b [= c implies a [= b -r> c ) :: thesis: ( a [= b -r> c implies a [*] b [= c )_{5}( Element of Q) -> Element of the carrier of Q = $1 [*] b;

defpred S_{1}[ set ] means $1 in X;

defpred S_{2}[ Element of Q] means $1 [*] b [= c;

assume a [= b -r> c ; :: thesis: a [*] b [= c

then A1: a [*] b [= ("\/" X) [*] b by Th8;

( S_{1}[d] iff S_{2}[d] )
;

A3: { H_{5}(d1) where d1 is Element of Q : S_{1}[d1] } = { H_{5}(d2) where d2 is Element of Q : S_{2}[d2] }
from FRAENKEL:sch 3(A2);

A4: { (d [*] b) where d is Element of Q : d in X } is_less_than c

then ("\/" X) [*] b [= c by A4, LATTICE3:def 21;

hence a [*] b [= c by A1, LATTICES:7; :: thesis: verum

( 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= H

proof

then reconsider X = { d where d is Element of Q : d [*] b [= c } as Subset of Q ;
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 H_{1}(Q) )

assume x in { d where d is Element of Q : d [*] b [= c } ; :: thesis: x in H_{1}(Q)

then ex d being Element of Q st

( x = d & d [*] b [= c ) ;

hence x in H_{1}(Q)
; :: thesis: verum

end;assume x in { d where d is Element of Q : d [*] b [= c } ; :: thesis: x in H

then ex d being Element of Q st

( x = d & d [*] b [= c ) ;

hence x in H

thus ( a [*] b [= c implies a [= b -r> c ) :: thesis: ( a [= b -r> c implies a [*] b [= c )

proof

deffunc H
assume
a [*] b [= c
; :: thesis: a [= b -r> c

then a in X ;

hence a [= b -r> c by LATTICE3:38; :: thesis: verum

end;then a in X ;

hence a [= b -r> c by LATTICE3:38; :: thesis: verum

defpred S

defpred S

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

then A2:
for d being Element of Q 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;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

( S

A3: { H

A4: { (d [*] b) where d is Element of Q : d in X } is_less_than c

proof

("\/" X) [*] b = "\/" ( { (d [*] b) where d is Element of Q : d in X } ,Q)
by Def6;
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;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

then ("\/" X) [*] b [= c by A4, LATTICE3:def 21;

hence a [*] b [= c by A1, LATTICES:7; :: thesis: verum