let x, Y, X be set ; :: thesis: ( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
( 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 Lm1, XBOOLE_1:11; :: thesis: verum