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