(
p
,
(
0.
(
TOPREAL
n
)
)
)
=
0
by
EUCLID_2:32
;
then
(
p
,
(
q

q
)
)
=
0
by
RLVECT_1:5
;
then
q
in
Plane
(
p
,
q
) ;
hence
(
TOPREAL
n
)

(
Plane
(
p
,
q
)
)
is non
empty
SubSpace
of
TOPREAL
n
;
:: thesis:
verum