let X be set ; :: thesis: ( X is empty implies X is trivial )
assume A1: 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 )
thus ( x in X & y in X implies x = y ) by A1; :: thesis: verum