let x, y, c be non pair set ; :: thesis: 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} ;
:: thesis: verum