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

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