let x be object ; :: thesis: for Y, X being set holds
( X \/ {x} c= Y iff ( x in Y & X c= Y ) )
let 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