let p be Point of (TOP-REAL 2); :: thesis: ( p <> 0. (TOP-REAL 2) implies |.p.| > 0 )
assume p <> 0. (TOP-REAL 2) ; :: thesis: |.p.| > 0
then |.p.| <> 0 by TOPRNS_1:25;
hence |.p.| > 0 ; :: thesis: verum