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