let x, y, c be object ; :: thesis: ( [<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) )

[<*x,y*>,'&'] in InnerVertices (1GateCircStr (<*x,y*>,'&')) by Th47;

then [<*x,y*>,'&'] in InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) by Th21;

then A1: [<*x,y*>,'&'] in InnerVertices (MajorityIStr (x,y,c)) by Th21;

[<*y,c*>,'&'] in InnerVertices (1GateCircStr (<*y,c*>,'&')) by Th47;

then [<*y,c*>,'&'] in InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) by Th21;

then A2: [<*y,c*>,'&'] in InnerVertices (MajorityIStr (x,y,c)) by Th21;

[<*c,x*>,'&'] in InnerVertices (1GateCircStr (<*c,x*>,'&')) by Th47;

then [<*c,x*>,'&'] in InnerVertices (MajorityIStr (x,y,c)) by Th21;

hence ( [<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) ) by A1, A2, Th21; :: thesis: verum

[<*x,y*>,'&'] in InnerVertices (1GateCircStr (<*x,y*>,'&')) by Th47;

then [<*x,y*>,'&'] in InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) by Th21;

then A1: [<*x,y*>,'&'] in InnerVertices (MajorityIStr (x,y,c)) by Th21;

[<*y,c*>,'&'] in InnerVertices (1GateCircStr (<*y,c*>,'&')) by Th47;

then [<*y,c*>,'&'] in InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) by Th21;

then A2: [<*y,c*>,'&'] in InnerVertices (MajorityIStr (x,y,c)) by Th21;

[<*c,x*>,'&'] in InnerVertices (1GateCircStr (<*c,x*>,'&')) by Th47;

then [<*c,x*>,'&'] in InnerVertices (MajorityIStr (x,y,c)) by Th21;

hence ( [<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) ) by A1, A2, Th21; :: thesis: verum