let n1, n2 be Nat; :: thesis: ( X in sequence_univers . n1 & ( for n being Nat st n < n1 holds
not X in sequence_univers . n ) & X in sequence_univers . n2 & ( for n being Nat st n < n2 holds
not X in sequence_univers . n ) implies n1 = n2 )
assume that
A8: ( X in sequence_univers . n1 & ( for n being Nat st n < n1 holds
not X in sequence_univers . n ) ) and
A9: ( X in sequence_univers . n2 & ( for n being Nat st n < n2 holds
not X in sequence_univers . n ) ) ; :: thesis: n1 = n2
n1 = n2

proof

assume n1 <> n2 ; :: thesis: contradiction
then ( n1 < n2 or n2 < n1 ) by XXREAL_0:1;
hence contradiction by A8, A9; :: thesis: verum

end;

hence n1 = n2 ; :: thesis: verum