let x, y, c be object ; :: thesis: InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation

( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (MajorityStr (x,y,c)) is Relation ) by Th58, Th67;

hence InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation by Th2, CIRCCOMB:47; :: thesis: verum

( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (MajorityStr (x,y,c)) is Relation ) by Th58, Th67;

hence InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation by Th2, CIRCCOMB:47; :: thesis: verum