let Y be Subset of X; :: thesis: Y is trivial
for x, y being set st x in Y & y in Y holds
x = y by ZFMISC_1:def 10;
hence Y is trivial by ZFMISC_1:def 10; :: thesis: verum