consider n being Element of NAT such that
A1: Following (s,n) is stable by B1, 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 A1; :: thesis: verum