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