let n1, n2 be Element of NAT ; :: thesis: ( Following s,n1 is stable & ( for n being Element of NAT st n < n1 holds
not Following s,n is stable ) & Following s,n2 is stable & ( for n being Element of NAT st n < n2 holds
not Following s,n is stable ) implies n1 = n2 )
assume that
A4: Following s,n1 is stable and
A5: ( ( for n being Element of NAT st n < n1 holds
not Following s,n is stable ) & Following s,n2 is stable ) and
A6: for n being Element of NAT st n < n2 holds
not Following s,n is stable ; :: thesis: n1 = n2
assume A7: n1 <> n2 ; :: thesis: contradiction

per cases ( n1 < n2 or n2 < n1 ) by A7, XXREAL_0:1;

suppose n1 < n2 ; :: thesis: contradiction

hence contradiction by A4, A6; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

end;