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 Th40;
hence ( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) ) by TARSKI:def 2; :: thesis: verum