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: ( not InputVertices (2GatesCircStr x,y,c,'xor' ) is with_pair & InnerVertices (2GatesCircStr x,y,c,'xor' ) is Relation ) by Th58, Th59;
A2: ( not InputVertices (MajorityStr x,y,c) is with_pair & InnerVertices (MajorityStr x,y,c) is Relation ) by Th67, Th68;
( InputVertices (2GatesCircStr x,y,c,'xor' ) = {x,y,c} & InputVertices (MajorityStr x,y,c) = {x,y,c} ) by Th57, Th75;
hence InputVertices (BitAdderWithOverflowStr x,y,c) = {x,y,c} \/ {x,y,c} by A1, A2, Th7
.= {x,y,c} ;
:: thesis: verum