theorem Th74: :: FACIRC_1:74

for x, y, c being non pair object holds
( x in InputVertices (MajorityStr (x,y,c)) & y in InputVertices (MajorityStr (x,y,c)) & c in InputVertices (MajorityStr (x,y,c)) )