let x be object ; :: thesis: for X being set holds
( not X \ {x} = {} or X = {} or X = {x} )
let X be set ; :: thesis: ( not X \ {x} = {} or X = {} or X = {x} )
assume X \ {x} = {} ; :: thesis: ( X = {} or X = {x} )
then X c= {x} by XBOOLE_1:37;
hence ( X = {} or X = {x} ) by Lm3; :: thesis: verum