let
E
be
Element
of
S
;
:: thesis:
E
is
Subset
of
X
per
cases
(
S
is
empty
or not
S
is
empty
)
;
suppose
S
is
empty
;
:: thesis:
E
is
Subset
of
X
then
E
is
empty
by
SUBSET_1:def 1
;
hence
E
is
Subset
of
X
by
SUBSET_1:1
;
:: thesis:
verum
end;
suppose
not
S
is
empty
;
:: thesis:
E
is
Subset
of
X
then
E
in
S
;
hence
E
is
Subset
of
X
;
:: thesis:
verum
end;
end;