theorem Th72: :: FACIRC_1:72

for x, y, c being object holds
( x in the carrier of (MajorityStr (x,y,c)) & y in the carrier of (MajorityStr (x,y,c)) & c in the carrier of (MajorityStr (x,y,c)) )