:: deftheorem defines MajorityOutput FACIRC_1:def 20 :
for x, y, c being object holds MajorityOutput (x,y,c) = [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];