let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: not LeftComp g is Bounded
A1: ((L~ g) \/ (RightComp g)) \/ (LeftComp g) = the carrier of (TOP-REAL 2) by Th25;
A2: RightComp g c= Cl (RightComp g) by PRE_TOPC:48;
Cl (RightComp g) is compact by Th42;
then RightComp g is Bounded by A2, JORDAN2C:16;
then (L~ g) \/ (RightComp g) is Bounded by TOPREAL6:76;
hence not LeftComp g is Bounded by A1, TOPREAL6:74; :: thesis: verum