let X be set ; :: thesis: ( X is empty implies X is trivial )
assume Z: X is empty ; :: thesis: X is trivial
let x be set ; :: according to ZFMISC_1:def 10 :: thesis: for y being set st x in X & y in X holds
x = y
let y be set ; :: thesis: ( x in X & y in X implies x = y )
X = {} by Z;
hence ( x in X & y in X implies x = y ) ; :: thesis: verum