let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: for x, y, c being non pair set holds not InputVertices (2GatesCircStr (x,y,c,f)) is with_pair
let x, y, c be non pair set ; :: thesis: not InputVertices (2GatesCircStr (x,y,c,f)) is with_pair
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by Th57;
hence not InputVertices (2GatesCircStr (x,y,c,f)) is with_pair ; :: thesis: verum