let X, x, Y be set ; :: thesis: ( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
A1: ( X \/ {x} c= Y implies ( X c= Y & {x} c= Y ) ) by XBOOLE_1:11;
( X c= Y & {x} c= Y implies X \/ {x} c= Y ) by XBOOLE_1:8;
hence ( X \/ {x} c= Y iff ( x in Y & X c= Y ) ) by A1, ZFMISC_1:37; :: thesis: verum