let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: RightComp g is_inside_component_of L~ g
thus RightComp g is_a_component_of (L~ g) ` by GOBOARD9:def 2; :: according to JORDAN2C:def 3 :: thesis: RightComp g is Bounded
Cl (RightComp g) is compact by Th42;
hence RightComp g is Bounded by JORDAN2C:16, PRE_TOPC:48; :: thesis: verum