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*>,'&' ) & [<*y,c*>,'&' ] in InnerVertices (1GateCircStr <*y,c*>,'&' ) ) by Th47;
then ( [<*c,x*>,'&' ] in InnerVertices (1GateCircStr <*c,x*>,'&' ) & [<*x,y*>,'&' ] in InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) & [<*y,c*>,'&' ] in InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) ) by Th21, Th47;
then ( [<*x,y*>,'&' ] in InnerVertices (MajorityIStr x,y,c) & [<*y,c*>,'&' ] in InnerVertices (MajorityIStr x,y,c) & [<*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 Th21; :: thesis: verum