let x, y, c be set ; :: 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