let g be V8() standard clockwise_oriented special_circular_sequence; :: thesis: RightComp g c= RightComp (SpStSeq (L~ g))
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in RightComp g or a in RightComp (SpStSeq (L~ g)) )
assume A1: a in RightComp g ; :: thesis: a in RightComp (SpStSeq (L~ g))
then reconsider p = a as Point of (TOP-REAL 2) ;
p `1 > W-bound (L~ g) by A1, Th23;
then A2: p `1 > W-bound (L~ (SpStSeq (L~ g))) by SPRECT_1:58;
p `2 > S-bound (L~ g) by A1, Th26;
then A3: p `2 > S-bound (L~ (SpStSeq (L~ g))) by SPRECT_1:59;
p `1 < E-bound (L~ g) by A1, Th24;
then A4: p `1 < E-bound (L~ (SpStSeq (L~ g))) by SPRECT_1:61;
p `2 < N-bound (L~ g) by A1, Th25;
then A5: p `2 < N-bound (L~ (SpStSeq (L~ g))) by SPRECT_1:60;
RightComp (SpStSeq (L~ g)) = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ (SpStSeq (L~ g))) < q `1 & q `1 < E-bound (L~ (SpStSeq (L~ g))) & S-bound (L~ (SpStSeq (L~ g))) < q `2 & q `2 < N-bound (L~ (SpStSeq (L~ g))) ) } by SPRECT_3:37;
hence a in RightComp (SpStSeq (L~ g)) by A2, A4, A3, A5; :: thesis: verum