let x be object ; :: thesis: for X, Y being set st Y c= X & not x in Y holds
Y c= X \ {x}
let X, Y 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 object ; :: 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;
hence y in X \ {x} by XBOOLE_0:def 5; :: thesis: verum