take
{}
L
;
:: thesis:
for
x
,
y
being
set
st
x
in
{}
L
&
y
in
{}
L
& not
[
x
,
y
]
in
R
& not
x
=
y
holds
[
y
,
x
]
in
R
thus
for
x
,
y
being
set
st
x
in
{}
L
&
y
in
{}
L
& not
[
x
,
y
]
in
R
& not
x
=
y
holds
[
y
,
x
]
in
R
;
:: thesis:
verum