consider n being Element of NAT such that
A2: Following (s,n) is stable by A1, Def1;
take Following (s,n) ; :: thesis: ( Following (s,n) is stable & ex n being Element of NAT st Following (s,n) = Following (s,n) )
thus ( Following (s,n) is stable & ex n being Element of NAT st Following (s,n) = Following (s,n) ) by A2; :: thesis: verum