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
A1: RightComp g c= Cl (RightComp g) by PRE_TOPC:48;
Cl (RightComp g) is compact by Th42;
hence RightComp g is Bounded by A1, JORDAN2C:16; :: thesis: verum