reconsider
f
=
id
D
as
UnOp
of
D
;
take
f
;
:: thesis:
for
x
,
y
being
Element
of
D
st
[
x
,
y
]
in
R
holds
[
(
f
.
x
)
,
(
f
.
y
)
]
in
R
let
x
,
y
be
Element
of
D
;
:: thesis:
(
[
x
,
y
]
in
R
implies
[
(
f
.
x
)
,
(
f
.
y
)
]
in
R
)
thus
(
[
x
,
y
]
in
R
implies
[
(
f
.
x
)
,
(
f
.
y
)
]
in
R
) ;
:: thesis:
verum