let x be object ; :: thesis: for Y, X being set holds
( not X c= Y \/ {x} or x in X or X c= Y )
let 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
X = X /\ (Y \/ {x}) by A1, XBOOLE_1:28
.= (X /\ Y) \/ (X /\ {x}) by XBOOLE_1:23
.= (X /\ Y) \/ {} by A2, Lm6, XBOOLE_0:def 7
.= X /\ Y ;
hence X c= Y by XBOOLE_1:17; :: thesis: verum