let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: Cl (RightComp g) is compact
Cl (RightComp (SpStSeq (L~ g))) = product (1,2 --> [.(W-bound (L~ (SpStSeq (L~ g)))),(E-bound (L~ (SpStSeq (L~ g)))).],[.(S-bound (L~ (SpStSeq (L~ g)))),(N-bound (L~ (SpStSeq (L~ g)))).]) by Th38;
then A1: Cl (RightComp (SpStSeq (L~ g))) is compact by TOPREAL6:87;
RightComp g c= RightComp (SpStSeq (L~ g)) by Th41;
hence Cl (RightComp g) is compact by A1, COMPTS_1:18, PRE_TOPC:49; :: thesis: verum