theorem :: SEQM_3:43

for n being Nat holds
( n > 1 iff ex m being Nat st
( n = m + 1 & m > 0 ) )