let f be non constant standard special_circular_sequence; :: thesis: BDD (L~ f) is connected
( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by Th1;
hence BDD (L~ f) is connected ; :: thesis: verum