let x, y, c be object ; 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; verum