let f be set ; :: thesis: for x, y being non pair set holds not InputVertices (1GateCircStr (<*x,y*>,f)) is with_pair
let x, y be non pair set ; :: thesis: not InputVertices (1GateCircStr (<*x,y*>,f)) is with_pair
set p = <*x,y*>;
let z be pair set ; :: 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