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:116;
then BDD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def 3;
hence ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by JORDAN1H:30; :: thesis: verum