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

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