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*>;
A1: InputVertices (1GateCircStr <*x,y*>,f) = {x,y} by Th40;
let z be pair set ; :: according to FACIRC_1:def 2 :: thesis: not z in InputVertices (1GateCircStr <*x,y*>,f)
assume z in InputVertices (1GateCircStr <*x,y*>,f) ; :: thesis: contradiction
hence contradiction by A1, TARSKI:def 2; :: thesis: verum