let Y, x, X be set ; :: thesis: ( not X c= Y \/ {x} or x in X or X c= Y )
assume that
A1: X c= Y \/ {x} and
A2: not x in X ; :: thesis: X c= Y
X = X /\ (Y \/ {x}) by A1, XBOOLE_1:28
.= (X /\ Y) \/ (X /\ {x}) by XBOOLE_1:23
.= (X /\ Y) \/ {} by A2, Lm7, XBOOLE_0:def 7
.= X /\ Y ;
hence X c= Y by XBOOLE_1:17; :: thesis: verum