let g be V8() standard clockwise_oriented special_circular_sequence; :: thesis: not LeftComp g is bounded
Cl (RightComp g) is compact by Th32;
then RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42;
then A1: (L~ g) \/ (RightComp g) is bounded by TOPREAL6:67;
((L~ g) \/ (RightComp g)) \/ (LeftComp g) = the carrier of (TOP-REAL 2) by Th15;
hence not LeftComp g is bounded by A1, TOPREAL6:66; :: thesis: verum