let x be object ; :: thesis: for X being set st x in X holds
(X \ {x}) \/ {x} = X
let X be set ; :: thesis: ( x in X implies (X \ {x}) \/ {x} = X )
assume A1: x in X ; :: thesis: (X \ {x}) \/ {x} = X
thus (X \ {x}) \/ {x} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= (X \ {x}) \/ {x}
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (X \ {x}) \/ {x} or y in X )
assume y in (X \ {x}) \/ {x} ; :: thesis: y in X
then ( y in X \ {x} or y in {x} ) by XBOOLE_0:def 3;
hence y in X by A1, Th55, TARSKI:def 1; :: thesis: verum
end;
thus X c= (X \ {x}) \/ {x} :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in (X \ {x}) \/ {x} )
assume y in X ; :: thesis: y in (X \ {x}) \/ {x}
then ( y in {x} or y in X \ {x} ) by XBOOLE_0:def 5;
hence y in (X \ {x}) \/ {x} by XBOOLE_0:def 3; :: thesis: verum
end;