defpred S₁[ Element of REAL ] means ex k being Element of NAT st $1 = - k;
consider IT being Subset of REAL such that
A1: for r being Element of REAL holds
( r in IT iff S₁[r] ) from SUBSET_1:sch 3();
take IT ; :: thesis: for r being Real holds
( r in IT iff ex k being Element of NAT st r = - k )
thus for r being Real holds
( r in IT iff ex k being Element of NAT st r = - k ) by A1; :: thesis: verum