let
p
,
q
be
Point
of
(
TOP-REAL
2
)
;
:: thesis:
(
p
`1
=
q
`1
&
p
`2
=
q
`2
implies
p
=
q
)
assume
(
p
`1
=
q
`1
&
p
`2
=
q
`2
) ;
:: thesis:
p
=
q
hence
p
=
|[
(
q
`1
)
,
(
q
`2
)
]|
by
EUCLID:53
.=
q
by
EUCLID:53
;
:: thesis:
verum