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;