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 )

A2: { b where b is Element of Q : b [= a } c= { c where c is Element of Q : c [*] (a -r> s) [= s }

hence a [= (a -r> s) -r> s by A2, LATTICE3:45; :: thesis: a [= (a -l> s) -l> s

a = "\/" ( { d where d is Element of Q : d [= a } ,Q) by LATTICE3:44;

hence a [= (a -l> s) -l> s by A6, LATTICE3:45; :: thesis: verum

( 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 )

A2: { b where b is Element of Q : b [= a } c= { c where c is Element of Q : c [*] (a -r> s) [= s }

proof

A6:
{ b where b is Element of Q : b [= a } c= { c where c is Element of Q : (a -l> s) [*] c [= s }
let x be object ; :: 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

A3: x = b and

A4: b [= a ;

(b -r> s) [*] b [= s by Th12;

then A5: b [*] (b -r> s) [= s by A1, Th15;

a -r> s [= b -r> s by A4, Th13;

then b [*] (a -r> s) [= b [*] (b -r> s) by Th8;

then b [*] (a -r> s) [= s by A5, LATTICES:7;

hence x in { c where c is Element of Q : c [*] (a -r> s) [= s } by A3; :: thesis: verum

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

A3: x = b and

A4: b [= a ;

(b -r> s) [*] b [= s by Th12;

then A5: b [*] (b -r> s) [= s by A1, Th15;

a -r> s [= b -r> s by A4, Th13;

then b [*] (a -r> s) [= b [*] (b -r> s) by Th8;

then b [*] (a -r> s) [= s by A5, LATTICES:7;

hence x in { c where c is Element of Q : c [*] (a -r> s) [= s } by A3; :: thesis: verum

proof

a = "\/" ( { d where d is Element of Q : d [= a } ,Q)
by LATTICE3:44;
let x be object ; :: 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

A7: x = b and

A8: b [= a ;

b [*] (b -l> s) [= s by Th11;

then A9: (b -l> s) [*] b [= s by A1, Th15;

a -l> s [= b -l> s by A8, Th13;

then (a -l> s) [*] b [= (b -l> s) [*] b by Th8;

then (a -l> s) [*] b [= s by A9, LATTICES:7;

hence x in { c where c is Element of Q : (a -l> s) [*] c [= s } by A7; :: thesis: verum

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

A7: x = b and

A8: b [= a ;

b [*] (b -l> s) [= s by Th11;

then A9: (b -l> s) [*] b [= s by A1, Th15;

a -l> s [= b -l> s by A8, Th13;

then (a -l> s) [*] b [= (b -l> s) [*] b by Th8;

then (a -l> s) [*] b [= s by A9, LATTICES:7;

hence x in { c where c is Element of Q : (a -l> s) [*] c [= s } by A7; :: thesis: verum

hence a [= (a -r> s) -r> s by A2, LATTICE3:45; :: thesis: a [= (a -l> s) -l> s

a = "\/" ( { d where d is Element of Q : d [= a } ,Q) by LATTICE3:44;

hence a [= (a -l> s) -l> s by A6, LATTICE3:45; :: thesis: verum