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:55;
A2: 1GateCircStr <*x,y*>,'&' tolerates 1GateCircStr <*y,c*>,'&' by CIRCCOMB:55;
InnerVertices (MajorityIStr x,y,c) = (InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' ))) \/ (InnerVertices (1GateCircStr <*c,x*>,'&' )) by A1, CIRCCOMB:15
.= ((InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices (1GateCircStr <*y,c*>,'&' ))) \/ (InnerVertices (1GateCircStr <*c,x*>,'&' )) by A2, CIRCCOMB:15
.= ({[<*x,y*>,'&' ]} \/ (InnerVertices (1GateCircStr <*y,c*>,'&' ))) \/ (InnerVertices (1GateCircStr <*c,x*>,'&' )) by CIRCCOMB:49
.= ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]}) \/ (InnerVertices (1GateCircStr <*c,x*>,'&' )) by CIRCCOMB:49
.= ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]}) \/ {[<*c,x*>,'&' ]} by CIRCCOMB:49
.= {[<*x,y*>,'&' ],[<*y,c*>,'&' ]} \/ {[<*c,x*>,'&' ]} by ENUMSET1:41
.= {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} by ENUMSET1:43 ;
hence InnerVertices (MajorityIStr x,y,c) = {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} ; :: thesis: verum