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