let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds

( p <> 0. (TOP-REAL n) iff |.p.| > 0 )

let p be Point of (TOP-REAL n); :: thesis: ( p <> 0. (TOP-REAL n) iff |.p.| > 0 )

( p <> 0. (TOP-REAL n) implies |.p.| > 0 )

( p <> 0. (TOP-REAL n) iff |.p.| > 0 )

let p be Point of (TOP-REAL n); :: thesis: ( p <> 0. (TOP-REAL n) iff |.p.| > 0 )

( p <> 0. (TOP-REAL n) implies |.p.| > 0 )

proof

hence
( p <> 0. (TOP-REAL n) iff |.p.| > 0 )
by Th37; :: thesis: verum
assume A1:
p <> 0. (TOP-REAL n)
; :: thesis: |.p.| > 0

( n in NAT & 0 <= |.p.| ) by Th36, ORDINAL1:def 12;

hence |.p.| > 0 by A1, TOPRNS_1:24, XXREAL_0:1; :: thesis: verum

end;( n in NAT & 0 <= |.p.| ) by Th36, ORDINAL1:def 12;

hence |.p.| > 0 by A1, TOPRNS_1:24, XXREAL_0:1; :: thesis: verum