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

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