let x, y, c be set ; :: thesis: InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}
A1: (1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) tolerates 1GateCircStr (<*c,x*>,'&') by CIRCCOMB:47;
A2: 1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*y,c*>,'&') by CIRCCOMB:47;
InnerVertices (MajorityIStr (x,y,c)) = (InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&'))) by A1, CIRCCOMB:11
.= ((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&'))) by A2, CIRCCOMB:11
.= ({[<*x,y*>,'&']} \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:42
.= ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:42
.= ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ {[<*c,x*>,'&']} by CIRCCOMB:42
.= {[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by ENUMSET1:3 ;
hence InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} ; :: thesis: verum