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