let n be Nat; :: thesis: ( n > 1 iff ex m being Nat st
( n = m + 1 & m > 0 ) )
thus ( n > 1 implies ex m being Nat st
( n = m + 1 & m > 0 ) ) :: thesis: ( ex m being Nat st
( n = m + 1 & m > 0 ) implies n > 1 )

proof

assume A1: 1 < n ; :: thesis: ex m being Nat st
( n = m + 1 & m > 0 )
then consider m being Nat such that
A2: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: ( n = m + 1 & m > 0 )
m <> 0 by A1, A2;
hence ( n = m + 1 & m > 0 ) by A2; :: thesis: verum

end;

given m being Nat such that A3: ( n = m + 1 & m > 0 ) ; :: thesis: n > 1
0 + 1 < n by A3, XREAL_1:6;
hence n > 1 ; :: thesis: verum