let f be set ; :: thesis: for x, y being non pair object holds InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs
let x, y be non pair object ; :: thesis: InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs
set p = <*x,y*>;
let z be pair object ; :: according to FACIRC_1:def 2 :: thesis: not z in InputVertices (1GateCircStr (<*x,y*>,f))
assume A1: z in InputVertices (1GateCircStr (<*x,y*>,f)) ; :: thesis: contradiction
InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y} by Th40;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum