let
p
,
q
be
Point
of
(
TOP-REAL
2
)
;
:: thesis:
<*
p
,
q
*>
is
unfolded
len
<*
p
,
q
*>
=
2
by
FINSEQ_1:44
;
hence
<*
p
,
q
*>
is
unfolded
by
Th26
;
:: thesis:
verum