let x, y, c be non pair object ; :: thesis: InputVertices (MajorityStr (x,y,c)) is without_pairs
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 object 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:43;
( 1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*c,x*>,'&') & 1GateCircStr (<*y,c*>,'&') tolerates 1GateCircStr (<*c,x*>,'&') ) by CIRCCOMB:43;
then A3: (1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) tolerates 1GateCircStr (<*c,x*>,'&') by A2, CIRCCOMB:3;
( InnerVertices (1GateCircStr (<*x,y*>,'&')) = {[<*x,y*>,'&']} & InnerVertices (1GateCircStr (<*y,c*>,'&')) = {[<*y,c*>,'&']} ) by CIRCCOMB:42;
then ( InnerVertices (1GateCircStr (<*c,x*>,'&')) = {[<*c,x*>,'&']} & InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} ) by A2, CIRCCOMB:11, CIRCCOMB:42;
then A4: InnerVertices (MajorityIStr (x,y,c)) = ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ {[<*c,x*>,'&']} by A3, CIRCCOMB:11
.= {[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by ENUMSET1:3 ;
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;
( InputVertices (1GateCircStr (<*x,y*>,'&')) is without_pairs & InputVertices (1GateCircStr (<*y,c*>,'&')) is without_pairs ) by Th41;
then A6: InputVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) is without_pairs by Th8, CIRCCOMB:47;
InputVertices (1GateCircStr (<*c,x*>,'&')) is without_pairs by Th41;
then A7: InputVertices (MajorityIStr (x,y,c)) is without_pairs by A6, Th8, CIRCCOMB:47;
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; :: thesis: verum