let N be ExtNat; :: thesis: ( N < 1 implies N = 0 )
assume A1: N < 1 ; :: thesis: N = 0
then N in NAT by Th5;
then reconsider n = N as Nat ;
n = 0 by A1, NAT_1:14;
hence N = 0 ; :: thesis: verum