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;