let Y be Subset of X; :: thesis: Y is trivial
let x, y be set ; :: according to ZFMISC_1:def 10 :: thesis: ( not x in Y or not y in Y or x = y )
assume ( x in Y & y in Y ) ; :: thesis: x = y
then ( x in X & y in X ) by Lm1;
hence x = y by ZFMISC_1:def 10; :: thesis: verum