let Q be Quantale; :: thesis: for s, a being Element of Q st s is cyclic holds
( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )
let s, a be Element of Q; :: thesis: ( s is cyclic implies ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s ) )
assume A1: s is cyclic ; :: thesis: ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )
{ b where b is Element of Q : b [= a } c= { c where c is Element of Q : c [*] (a -r> s) [= s }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { b where b is Element of Q : b [= a } or x in { c where c is Element of Q : c [*] (a -r> s) [= s } )
assume x in { b where b is Element of Q : b [= a } ; :: thesis: x in { c where c is Element of Q : c [*] (a -r> s) [= s }
then consider b being Element of Q such that
A2: ( x = b & b [= a ) ;
( a -r> s [= b -r> s & (b -r> s) [*] b [= s ) by A2, Th12, Th13;
then ( b [*] (a -r> s) [= b [*] (b -r> s) & b [*] (b -r> s) [= s ) by A1, Th8, Th15;
then b [*] (a -r> s) [= s by LATTICES:25;
hence x in { c where c is Element of Q : c [*] (a -r> s) [= s } by A2; :: thesis: verum

end;

then ( a = "\/" { d where d is Element of Q : d [= a } ,Q & "\/" { b where b is Element of Q : b [= a } ,Q [= "\/" { c where c is Element of Q : c [*] (a -r> s) [= s } ,Q ) by LATTICE3:45, LATTICE3:46;
hence a [= (a -r> s) -r> s ; :: thesis: a [= (a -l> s) -l> s
{ b where b is Element of Q : b [= a } c= { c where c is Element of Q : (a -l> s) [*] c [= s }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { b where b is Element of Q : b [= a } or x in { c where c is Element of Q : (a -l> s) [*] c [= s } )
assume x in { b where b is Element of Q : b [= a } ; :: thesis: x in { c where c is Element of Q : (a -l> s) [*] c [= s }
then consider b being Element of Q such that
A3: ( x = b & b [= a ) ;
( a -l> s [= b -l> s & b [*] (b -l> s) [= s ) by A3, Th11, Th13;
then ( (a -l> s) [*] b [= (b -l> s) [*] b & (b -l> s) [*] b [= s ) by A1, Th8, Th15;
then (a -l> s) [*] b [= s by LATTICES:25;
hence x in { c where c is Element of Q : (a -l> s) [*] c [= s } by A3; :: thesis: verum

end;

then ( a = "\/" { d where d is Element of Q : d [= a } ,Q & "\/" { b where b is Element of Q : b [= a } ,Q [= "\/" { c where c is Element of Q : (a -l> s) [*] c [= s } ,Q ) by LATTICE3:45, LATTICE3:46;
hence a [= (a -l> s) -l> s ; :: thesis: verum