let x, y, c be non pair set ; :: thesis: InputVertices (BorrowStr (x,y,c)) is without_pairs
set M = BorrowStr (x,y,c);
set MI = BorrowIStr (x,y,c);
set S = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3);
given xx being pair object such that A1: xx in InputVertices (BorrowStr (x,y,c)) ; :: according to FACIRC_1:def 2 :: thesis: contradiction
A2: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47;
A3: ( InnerVertices (1GateCircStr (<*x,c*>,and2a)) = {[<*x,c*>,and2a]} & (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) tolerates 1GateCircStr (<*x,c*>,and2a) ) by CIRCCOMB:42, CIRCCOMB:47;
( InnerVertices (1GateCircStr (<*x,y*>,and2a)) = {[<*x,y*>,and2a]} & InnerVertices (1GateCircStr (<*y,c*>,and2)) = {[<*y,c*>,and2]} ) by CIRCCOMB:42;
then InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A2, CIRCCOMB:11;
then A4: InnerVertices (BorrowIStr (x,y,c)) = ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} by A3, CIRCCOMB:11
.= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by ENUMSET1:3 ;
InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by FACIRC_1:42;
then A5: (InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c))) = {} by A4, XBOOLE_1:37;
( InputVertices (1GateCircStr (<*x,y*>,and2a)) is without_pairs & InputVertices (1GateCircStr (<*y,c*>,and2)) is without_pairs ) by FACIRC_1:41;
then ( InputVertices (1GateCircStr (<*x,c*>,and2a)) is without_pairs & InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is without_pairs ) by FACIRC_1:9, FACIRC_1:41;
then A6: InputVertices (BorrowIStr (x,y,c)) is without_pairs by FACIRC_1:9;
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation by FACIRC_1:38;
then InputVertices (BorrowStr (x,y,c)) = (InputVertices (BorrowIStr (x,y,c))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c)))) by A6, FACIRC_1:6;
hence contradiction by A6, A1, A5; :: thesis: verum