let x, y, c be object ; :: 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:47;
InnerVertices (1GateCircStr (<*c,x*>,'&')) is Relation by Th38;
then InnerVertices (MajorityIStr (x,y,c)) is Relation by A2, Th2, CIRCCOMB:47;
hence InnerVertices (MajorityStr (x,y,c)) is Relation by A1, Th2, CIRCCOMB:47; :: thesis: verum