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: ( InputVertices (CompStr (x,b)) = {x,b} & InputVertices (IncrementStr (x,b)) = {x,b} ) by FACIRC_1:40;
( InnerVertices (CompStr (x,b)) is Relation & InnerVertices (IncrementStr (x,b)) is Relation ) by FACIRC_1:38;
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