let X, Y, 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
A3: X misses {x} by A2, ZFMISC_1:50;
X = X /\ (Y \/ {x}) by A1, XBOOLE_1:28
.= (X /\ Y) \/ (X /\ {x}) by XBOOLE_1:23
.= (X /\ Y) \/ {} by A3, XBOOLE_0:def 7
.= X /\ Y ;
hence X c= Y by XBOOLE_1:17; :: thesis: verum