let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )
let p be Point of (TOP-REAL n); :: thesis: ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )
( p <> 0. (TOP-REAL n) implies |(p,p)| > 0 )

proof

assume p <> 0. (TOP-REAL n) ; :: thesis: |(p,p)| > 0
then A1: |(p,p)| <> 0 by Th39;
0 <= |(p,p)| by Th33;
hence |(p,p)| > 0 by A1, XXREAL_0:1; :: thesis: verum

end;

hence ( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 ) by Th39; :: thesis: verum