let n be non zero Nat; :: thesis: ( n <> 1 implies n >= 2 )
assume A1: n <> 1 ; :: thesis: n >= 2
assume n < 2 ; :: thesis: contradiction
then n < 1 + 1 ;
then n <= 0 + 1 by NAT_1:13;
hence contradiction by A1, NAT_1:8; :: thesis: verum