sqr p = p (#) p ;
hence p ^2 is Point of (TOP-REAL n) ; :: thesis: verum