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

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