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