let g be V8() 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 Th28;
then A1: Cl (RightComp (SpStSeq (L~ g))) is compact by TOPREAL6:78;
RightComp g c= RightComp (SpStSeq (L~ g)) by Th31;
hence Cl (RightComp g) is compact by A1, COMPTS_1:9, PRE_TOPC:19; :: thesis: verum