let x, X be set ; :: thesis: ( {x} \ X = {} or {x} \ X = {x} )
assume {x} \ X <> {} ; :: thesis: {x} \ X = {x}
then not x in X by Lm11;
hence {x} \ X = {x} by Lm10; :: thesis: verum