let g be V8() 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 2 :: thesis: RightComp g is bounded
Cl (RightComp g) is compact by Th32;
hence RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; :: thesis: verum