set
t1
= the
Element
of
T
;
consider
s1
,
s2
being
Element
of
S
such that
A1
:
s1
<>
s2
by
SUBSET_1:def 7
;
per
cases
(
s1
=
the
Element
of
T
or
s1
<>
the
Element
of
T
)
;
suppose
s1
=
the
Element
of
T
;
:: thesis:
not
DiffElems
(
S
,
T
) is
empty
then
[
s2
, the
Element
of
T
]
in
DiffElems
(
S
,
T
)
by
A1
;
hence
not
DiffElems
(
S
,
T
) is
empty
;
:: thesis:
verum
end;
suppose
s1
<>
the
Element
of
T
;
:: thesis:
not
DiffElems
(
S
,
T
) is
empty
then
[
s1
, the
Element
of
T
]
in
DiffElems
(
S
,
T
) ;
hence
not
DiffElems
(
S
,
T
) is
empty
;
:: thesis:
verum
end;
end;