theorem Th3: :: FLANG_2:3

for m, n being Nat st m < n holds
ex k being Nat st
( m + k = n & k > 0 )