let x, y, c be set ; :: thesis: InnerVertices (MajorityStr x,y,c) is Relation
A1: ( InnerVertices (1GateCircStr <*x,y*>,'&' ) is Relation & InnerVertices (1GateCircStr <*c,x*>,'&' ) is Relation & InnerVertices (1GateCircStr <*y,c*>,'&' ) is Relation ) by Th38;
then InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) is Relation by Th2, CIRCCOMB:55;
then ( InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ) is Relation & InnerVertices (MajorityIStr x,y,c) is Relation ) by A1, Th3, Th38;
hence InnerVertices (MajorityStr x,y,c) is Relation by Th2, CIRCCOMB:55; :: thesis: verum