set
a
= the
Point
of
RAS
;
take
Phi
( the
Point
of
RAS
,
x
) ;
:: thesis:
for
a
being
Point
of
RAS
holds
Phi
( the
Point
of
RAS
,
x
)
=
Phi
(
a
,
x
)
thus
for
a
being
Point
of
RAS
holds
Phi
( the
Point
of
RAS
,
x
)
=
Phi
(
a
,
x
)
by
Th22
;
:: thesis:
verum