let n be non zero Nat; :: thesis: ( n <> 1 implies n > 1 )
A1: n >= 1 by NAT_1:14;
assume n <> 1 ; :: thesis: n > 1
hence n > 1 by A1, XXREAL_0:1; :: thesis: verum