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 A1: 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 a [= (a -r> s) -r> s by Th16;
then A2: ((a -r> s) -r> s) -r> s [= a -r> s by Th13;
a [= (a -l> s) -l> s by A1, Th16;
then A3: ((a -l> s) -l> s) -l> s [= a -l> s by Th13;
( a -r> s [= ((a -r> s) -r> s) -r> s & a -l> s [= ((a -l> s) -l> s) -l> s ) by A1, Th16;
hence ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) by A2, A3, LATTICES:8; :: thesis: verum