let f be non constant standard special_circular_sequence; :: thesis: ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f )
UBD (L~ f) is_outside_component_of L~ f by JORDAN2C:68;
then UBD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def 3;
hence ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) by JORDAN1H:24; :: thesis: verum