let
x
,
y
be
Element
of
REAL
;
:: thesis:
real_dist
.
(
x
,
y
)
=
real_dist
.
(
y
,
x
)
thus
real_dist
.
(
x
,
y
) =
.
(
x

y
)
.
by
Def12
.=
.
(

(
x

y
)
)
.
by
COMPLEX1:52
.=
.
(
y

x
)
.
.=
real_dist
.
(
y
,
x
)
by
Def12
;
:: thesis:
verum