let x, b be non pair set ; :: thesis: ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) )
InputVertices (CompStr (x,b)) = {x,b} by FACIRC_1:40;
hence ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) ) by TARSKI:def 2; :: thesis: verum