A1: x in NAT by ORDINAL1:def 12;

hereby :: thesis: ( not x <> 0 implies ex b₁ being Element of NAT st b₁ = 0 )

assume x <> 0 ; :: thesis: ex k1, m being Element of NAT st
( m ! <= x & x < (m + 1) ! & k1 = m ! )
then x >= 0 + 1 by NAT_1:13;
then consider k being Element of NAT such that
A2: k ! <= x and
A3: x < (k + 1) ! and
for m being Element of NAT st m ! <= x & x < (m + 1) ! holds
m = k by Lm52, A1;
consider k1 being Real such that
A4: k1 = k ! ;
reconsider k1 = k1 as Element of NAT by A4;
take k1 = k1; :: thesis: ex m being Element of NAT st
( m ! <= x & x < (m + 1) ! & k1 = m ! )
thus ex m being Element of NAT st
( m ! <= x & x < (m + 1) ! & k1 = m ! ) by A2, A3, A4; :: thesis: verum

end;

thus ( not x <> 0 implies ex b₁ being Element of NAT st b₁ = 0 ) ; :: thesis: verum