let Y, X, x be set ; :: thesis: ( Y c= X & not x in Y implies Y c= X \ {x} )
assume A1: ( Y c= X & not x in Y ) ; :: thesis: Y c= X \ {x}
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in X \ {x} )
assume y in Y ; :: thesis: y in X \ {x}
then ( y in X & not y in {x} ) by A1, TARSKI:def 1, TARSKI:def 3;
hence y in X \ {x} by XBOOLE_0:def 5; :: thesis: verum