:: deftheorem Def1 defines MajP BINARI_4:def 1 :
for m, j, b₃ being Nat holds
( b₃ = MajP (m,j) iff ( 2 to_power b₃ >= j & b₃ >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b₃ ) ) );