defpred S₁[ Nat] means Following (s,$1) is stable ;
ex k being Element of NAT st S₁[k] by A1;
then A2: ex k being Nat st S₁[k] ;
consider m being Nat such that
A3: ( S₁[m] & ( for n being Nat st S₁[n] holds
m <= n ) ) from NAT_1:sch 5(A2);
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: ( Following (s,m) is stable & ( for n being Element of NAT st n < m holds
not Following (s,n) is stable ) )
thus ( Following (s,m) is stable & ( for n being Element of NAT st n < m holds
not Following (s,n) is stable ) ) by A3; :: thesis: verum