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

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