let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: BDD (L~ g) = RightComp g
( UBD (L~ g) = LeftComp g & (L~ g) ` = (LeftComp g) \/ (RightComp g) & (L~ g) ` = (BDD (L~ g)) \/ (UBD (L~ g)) & LeftComp g misses RightComp g & BDD (L~ g) misses UBD (L~ g) ) by Th24, Th46, GOBRD12:11, JORDAN2C:28, JORDAN2C:31;
hence BDD (L~ g) = RightComp g by XBOOLE_1:71; :: thesis: verum