let x, y, c be non pair object ; InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}
set S = BitAdderWithOverflowStr (x,y,c);
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = MajorityStr (x,y,c);
A1:
( InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} & InputVertices (MajorityStr (x,y,c)) = {x,y,c} )
by Th57, Th75;
( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (MajorityStr (x,y,c)) is Relation )
by Th58, Th67;
hence InputVertices (BitAdderWithOverflowStr (x,y,c)) =
{x,y,c} \/ {x,y,c}
by A1, Th7
.=
{x,y,c}
;
verum