{}
is
Element
of
Fin
X
by
FINSUB_1:7
;
then
reconsider
b
=
[
{}
,
{}
]
as
Element
of
[:
(
Fin
X
)
,
(
Fin
X
)
:]
by
ZFMISC_1:def 2
;
b
`1
misses
b
`2
;
then
b
in
{
a
where
a
is
Element
of
[:
(
Fin
X
)
,
(
Fin
X
)
:]
:
a
`1
misses
a
`2
}
;
hence
not
DISJOINT_PAIRS
X
is
empty
;
:: thesis:
verum