let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: LeftComp g is_outside_component_of L~ g
thus LeftComp g is_a_component_of (L~ g) ` by GOBOARD9:def 1; :: according to JORDAN2C:def 4 :: thesis: not LeftComp g is Bounded
thus not LeftComp g is Bounded by Th43; :: thesis: verum