let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: RightComp g c= RightComp (SpStSeq (L~ g))
let a be set ; :: 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) & p `1 < E-bound (L~ g) & p `2 > S-bound (L~ g) & p `2 < N-bound (L~ g) ) by A1, Th33, Th34, Th35, Th36;
then A2: ( p `1 > W-bound (L~ (SpStSeq (L~ g))) & p `1 < E-bound (L~ (SpStSeq (L~ g))) & p `2 > S-bound (L~ (SpStSeq (L~ g))) & p `2 < N-bound (L~ (SpStSeq (L~ g))) ) by SPRECT_1:66, SPRECT_1:67, SPRECT_1:68, SPRECT_1:69;
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:54;
hence a in RightComp (SpStSeq (L~ g)) by A2; :: thesis: verum