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