let x, y, c be non pair set ; :: thesis: not InputVertices (MajorityStr x,y,c) is with_pair
set M = MajorityStr x,y,c;
set MI = MajorityIStr x,y,c;
set S = 1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ;
given xx being pair set such that A1: xx in InputVertices (MajorityStr x,y,c) ; :: according to FACIRC_1:def 2 :: thesis: contradiction
A2: 1GateCircStr <*x,y*>,'&' tolerates 1GateCircStr <*y,c*>,'&' by CIRCCOMB:51;
( 1GateCircStr <*x,y*>,'&' tolerates 1GateCircStr <*c,x*>,'&' & 1GateCircStr <*y,c*>,'&' tolerates 1GateCircStr <*c,x*>,'&' ) by CIRCCOMB:51;
then A3: (1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' ) tolerates 1GateCircStr <*c,x*>,'&' by A2, CIRCCOMB:7;
( InnerVertices (1GateCircStr <*x,y*>,'&' ) = {[<*x,y*>,'&' ]} & InnerVertices (1GateCircStr <*y,c*>,'&' ) = {[<*y,c*>,'&' ]} ) by CIRCCOMB:49;
then ( InnerVertices (1GateCircStr <*c,x*>,'&' ) = {[<*c,x*>,'&' ]} & InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) = {[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]} ) by A2, CIRCCOMB:15, CIRCCOMB:49;
then A4: InnerVertices (MajorityIStr x,y,c) = ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]}) \/ {[<*c,x*>,'&' ]} by A3, CIRCCOMB:15
.= {[<*x,y*>,'&' ],[<*y,c*>,'&' ]} \/ {[<*c,x*>,'&' ]} by ENUMSET1:41
.= {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} by ENUMSET1:43 ;
InputVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ) = {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} by Th42;
then A5: (InputVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) \ (InnerVertices (MajorityIStr x,y,c)) = {} by A4, XBOOLE_1:37;
( not InputVertices (1GateCircStr <*x,y*>,'&' ) is with_pair & not InputVertices (1GateCircStr <*y,c*>,'&' ) is with_pair ) by Th41;
then A6: not InputVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) is with_pair by Th8, CIRCCOMB:55;
not InputVertices (1GateCircStr <*c,x*>,'&' ) is with_pair by Th41;
then A7: not InputVertices (MajorityIStr x,y,c) is with_pair by A6, Th8, CIRCCOMB:55;
InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ) is Relation by Th38;
then InputVertices (MajorityStr x,y,c) = (InputVertices (MajorityIStr x,y,c)) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) \ (InnerVertices (MajorityIStr x,y,c))) by A7, Th6;
hence contradiction by A7, A1, A5, Def2; :: thesis: verum