let
A
be
set
;
:: thesis:
[
{}
,
{}
]
is
Element
of
DISJOINT_PAIRS
A
(
[
{}
,
{}
]
=
[
(
{}.
A
)
,
(
{}.
A
)
]
&
[
{}
,
{}
]
`1
misses
[
{}
,
{}
]
`2
) ;
hence
[
{}
,
{}
]
is
Element
of
DISJOINT_PAIRS
A
by
NORMFORM:29
;
:: thesis:
verum