let Q be Quantale; :: thesis: for s, a being Element of Q st s is cyclic holds
( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s )
let s, a be Element of Q; :: thesis: ( s is cyclic implies ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) )
assume s is cyclic ; :: thesis: ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s )
then A1: ( a [= (a -r> s) -r> s & a -r> s [= ((a -r> s) -r> s) -r> s & a [= (a -l> s) -l> s & a -l> s [= ((a -l> s) -l> s) -l> s ) by Th16;
then ( ((a -r> s) -r> s) -r> s [= a -r> s & ((a -l> s) -l> s) -l> s [= a -l> s ) by Th13;
hence ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) by A1, LATTICES:26; :: thesis: verum