theorem :: ABCMIZ_A:46

for m being constructor binary OperSymbol of MaxConstrSign
for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m