defpred
S
_{1}
[
Point
of
(
TOPREAL
2
)
]
means
.
(
$1

[
a
,
b
]
)
.
>
r
;
{
p
where
p
is
Point
of
(
TOPREAL
2
)
:
S
_{1}
[
p
] }
c=
the
carrier
of
(
TOPREAL
2
)
from
FRAENKEL:sch 10
();
hence
{
p
where
p
is
Point
of
(
TOPREAL
2
)
:
.
(
p

[
a
,
b
]
)
.
>
r
} is
Subset
of
(
TOPREAL
2
)
;
:: thesis:
verum