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