let g be V8() standard clockwise_oriented special_circular_sequence; :: thesis: BDD (L~ g) = RightComp g
A1: BDD (L~ g) misses UBD (L~ g) by JORDAN2C:24;
A2: ( (L~ g) ` = (BDD (L~ g)) \/ (UBD (L~ g)) & LeftComp g misses RightComp g ) by Th14, JORDAN2C:27;
( UBD (L~ g) = LeftComp g & (L~ g) ` = (LeftComp g) \/ (RightComp g) ) by Th36, GOBRD12:10;
hence BDD (L~ g) = RightComp g by A2, A1, XBOOLE_1:71; :: thesis: verum