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 & ( for n being Element of NAT st n < n1 holds
not Following s,n is stable ) ) and
A5: ( Following s,n2 is stable & ( for n being Element of NAT st n < n2 holds
not Following s,n is stable ) ) ; :: thesis: n1 = n2
assume A6: n1 <> n2 ; :: thesis: contradiction

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

suppose n1 < n2 ; :: thesis: contradiction

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

end;

suppose n2 < n1 ; :: thesis: contradiction

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

end;

end;