let Q be Quantale; :: thesis: for c being Element of Q holds
( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c )
let c be Element of Q; :: thesis: ( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c )
thus ( c is cyclic implies for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c ) :: thesis: ( ( for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c ) implies c is cyclic )

proof

assume A1: for a being Element of Q holds a -r> c = a -l> c ; :: according to QUANTAL1:def 18 :: thesis: for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c
let a, b be Element of Q; :: thesis: ( a [*] b [= c implies b [*] a [= c )
assume a [*] b [= c ; :: thesis: b [*] a [= c
then a [= b -r> c by Th12;
then a [= b -l> c by A1;
hence b [*] a [= c by Th11; :: thesis: verum

end;

assume A2: for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c ; :: thesis: c is cyclic
let a be Element of Q; :: according to QUANTAL1:def 18 :: thesis: a -r> c = a -l> c
set X1 = { d1 where d1 is Element of Q : d1 [*] a [= c } ;
set X2 = { d2 where d2 is Element of Q : a [*] d2 [= c } ;
{ d1 where d1 is Element of Q : d1 [*] a [= c } = { d2 where d2 is Element of Q : a [*] d2 [= c }

proof

thus { d1 where d1 is Element of Q : d1 [*] a [= c } c= { d2 where d2 is Element of Q : a [*] d2 [= c } :: according to XBOOLE_0:def 10 :: thesis: { d2 where d2 is Element of Q : a [*] d2 [= c } c= { d1 where d1 is Element of Q : d1 [*] a [= c }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d1 where d1 is Element of Q : d1 [*] a [= c } or x in { d2 where d2 is Element of Q : a [*] d2 [= c } )
assume x in { d1 where d1 is Element of Q : d1 [*] a [= c } ; :: thesis: x in { d2 where d2 is Element of Q : a [*] d2 [= c }
then consider d being Element of Q such that
A3: x = d and
A4: d [*] a [= c ;
a [*] d [= c by A2, A4;
hence x in { d2 where d2 is Element of Q : a [*] d2 [= c } by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d2 where d2 is Element of Q : a [*] d2 [= c } or x in { d1 where d1 is Element of Q : d1 [*] a [= c } )
assume x in { d2 where d2 is Element of Q : a [*] d2 [= c } ; :: thesis: x in { d1 where d1 is Element of Q : d1 [*] a [= c }
then consider d being Element of Q such that
A5: x = d and
A6: a [*] d [= c ;
d [*] a [= c by A2, A6;
hence x in { d1 where d1 is Element of Q : d1 [*] a [= c } by A5; :: thesis: verum

end;

hence a -r> c = a -l> c ; :: thesis: verum