given g1, g2 being Point of (TOP-REAL N) such that A2: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < r and
A3: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g2).| < r and
A4: g1 <> g2 ; :: thesis: contradiction

A5: now

assume |.(g1 - g2).| = 0 ; :: thesis: contradiction
then (0. (TOP-REAL N)) + g2 = (g1 - g2) + g2 by Th25;
then g2 = (g1 - g2) + g2 by EUCLID:27
.= g1 - (g2 - g2) by EUCLID:47
.= g1 - (0. (TOP-REAL N)) by EUCLID:42
.= g1 + (- (0. (TOP-REAL N))) by EUCLID:41
.= g1 + ((- 1) * (0. (TOP-REAL N))) by EUCLID:39
.= g1 + (0. (TOP-REAL N)) by EUCLID:28
.= g1 by EUCLID:27 ;
hence contradiction by A4; :: thesis: verum

end;

then consider n1 being Element of NAT such that
A6: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < |.(g1 - g2).| / 4 by A2, XREAL_1:224;
consider n2 being Element of NAT such that
A7: for m being Element of NAT st n2 <= m holds
|.((seq . m) - g2).| < |.(g1 - g2).| / 4 by A3, A5, XREAL_1:224;
A8: |.((seq . (n1 + n2)) - g2).| < |.(g1 - g2).| / 4 by A7, NAT_1:12;
|.((seq . (n1 + n2)) - g1).| < |.(g1 - g2).| / 4 by A6, NAT_1:12;
then A9: |.((seq . (n1 + n2)) - g2).| + |.((seq . (n1 + n2)) - g1).| < (|.(g1 - g2).| / 4) + (|.(g1 - g2).| / 4) by A8, XREAL_1:8;
|.(g1 - g2).| = |.((g1 - g2) + (0. (TOP-REAL N))).| by EUCLID:27
.= |.((g1 - g2) + ((- 1) * (0. (TOP-REAL N)))).| by EUCLID:28
.= |.((g1 - g2) + (- (0. (TOP-REAL N)))).| by EUCLID:39
.= |.((g1 - g2) - (0. (TOP-REAL N))).| by EUCLID:41
.= |.((g1 - g2) - ((seq . (n1 + n2)) - (seq . (n1 + n2)))).| by EUCLID:42
.= |.(((g1 - g2) - (seq . (n1 + n2))) + (seq . (n1 + n2))).| by EUCLID:47
.= |.((g1 - ((seq . (n1 + n2)) + g2)) + (seq . (n1 + n2))).| by EUCLID:46
.= |.(((g1 - (seq . (n1 + n2))) - g2) + (seq . (n1 + n2))).| by EUCLID:46
.= |.((g1 - (seq . (n1 + n2))) - (g2 - (seq . (n1 + n2)))).| by EUCLID:47
.= |.((g1 - (seq . (n1 + n2))) + (- (g2 - (seq . (n1 + n2))))).| by EUCLID:41
.= |.((g1 - (seq . (n1 + n2))) + ((seq . (n1 + n2)) - g2)).| by EUCLID:44
.= |.((- ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).| by EUCLID:44 ;
then |.(g1 - g2).| <= |.(- ((seq . (n1 + n2)) - g1)).| + |.((seq . (n1 + n2)) - g2).| by Th30;
then A10: |.(g1 - g2).| <= |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).| by EUCLID:71;
|.(g1 - g2).| / 2 < |.(g1 - g2).| by A5, XREAL_1:216;
hence contradiction by A9, A10, XXREAL_0:2; :: thesis: verum