let g be constant standard clockwise_oriented special_circular_sequence; :: thesis: UBD (L~ g) = LeftComp g
( UBD (L~ g) is_outside_component_of L~ g & LeftComp g is_outside_component_of L~ g ) by Th34, JORDAN2C:68;
hence UBD (L~ g) = LeftComp g by JORDAN2C:119; :: thesis: verum