let x, b be non pair set ; :: thesis: InputVertices (BitCompStr x,b) = {x,b}
set S1 = CompStr x,b;
set S2 = IncrementStr x,b;
set S = BitCompStr x,b;
A1: ( InnerVertices (CompStr x,b) is Relation & InnerVertices (IncrementStr x,b) is Relation ) by FACIRC_1:38;
( InputVertices (CompStr x,b) = {x,b} & InputVertices (IncrementStr x,b) = {x,b} ) by FACIRC_1:40;
then InputVertices (BitCompStr x,b) = {x,b} \/ {x,b} by A1, FACIRC_1:7
.= {x,b} ;
hence InputVertices (BitCompStr x,b) = {x,b} ; :: thesis: verum