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 )

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 }

( 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 A2:
for a, b being Element of Q st a [*] b [= c holds
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;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

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

hence
a -r> c = a -l> c
; :: thesis: verum
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 }

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;proof

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 } )
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;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

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