let j be Element of NAT ; :: thesis: ( j < 1 implies j = 0 )
assume j < 1 ; :: thesis: j = 0
then j < 0 + 1 ;
hence j = 0 by NAT_1:13; :: thesis: verum