let Y be Subset of X; :: thesis: Y is trivial
let x, y be Element of Y; :: according to SUBSET_1:def 7 :: thesis: x = y

per cases ( not Y is empty or Y is empty ) ;

suppose not Y is empty ; :: thesis: x = y

then ( x in Y & y in Y ) by Def1;
then ( x in X & y in X ) by Lm1;
hence x = y by ZFMISC_1:def 10; :: thesis: verum

end;

suppose Y is empty ; :: thesis: x = y

then ( x = {} & y = {} ) by Def1;
hence x = y ; :: thesis: verum

end;

end;