let f be non constant standard special_circular_sequence; :: thesis: ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f )
BDD (L~ f) is_inside_component_of L~ f by JORDAN2C:108;
then BDD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def 2;
hence ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by JORDAN1H:24; :: thesis: verum