theorem :: BINARI_4:23

for m being Nat st m >= 1 holds
MajP (m,1) = m