let
x
,
y
be
Real
;
:: thesis:
(
[
x
,
y
]
in
realantidiagonal
implies
y
=

x
)
assume
[
x
,
y
]
in
realantidiagonal
;
:: thesis:
y
=

x
then
consider
x1
,
y1
being
Real
such that
A1
:
[
x
,
y
]
=
[
x1
,
y1
]
and
A2
:
y1
=

x1
;
(
x
=
x1
&
y
=
y1
)
by
A1
,
XTUPLE_0:1
;
hence
y
=

x
by
A2
;
:: thesis:
verum