reconsider m1 = IC s as Element of NAT ;
consider k being Element of NAT such that
A1: m1 = k ;
reconsider m = abs (k + c) as Nat ;
reconsider l = m as Element of NAT ;
take l ; :: thesis: ex m being Element of NAT st
( m = IC s & l = abs (m + c) )
thus ex m being Element of NAT st
( m = IC s & l = abs (m + c) ) by A1; :: thesis: verum