for x, y, c being object holds
( BitAdderOutput (x,y,c) in InnerVertices (BitAdderWithOverflowStr (x,y,c)) & MajorityOutput (x,y,c) in InnerVertices (BitAdderWithOverflowStr (x,y,c)) ) by Th21;