consider
i
,
j
being
Element
of
I
such that
A1
:
i
<>
j
by
LMXorDelta
;
[
i
,
j
]
in
{
[
i
,
j
]
where
i
,
j
is
Element
of
I
:
i
<>
j
}
by
A1
;
hence
{
[
i
,
j
]
where
i
,
j
is
Element
of
I
:
i
<>
j
} is non
empty
set
;
:: thesis:
verum