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 )

( 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

hence
( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )
by Th39; :: thesis: verum
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;then A1: |(p,p)| <> 0 by Th39;

0 <= |(p,p)| by Th33;

hence |(p,p)| > 0 by A1, XXREAL_0:1; :: thesis: verum