reconsider
f
=
p
as
Element
of
REAL
n
by
EUCLID:22
;
f
(/)
r
is
Element
of
REAL
n
;
hence
p
(/)
r
is
Point
of
(
TOP-REAL
n
)
by
EUCLID:22
;
:: thesis:
verum