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