let x, y be object ; :: thesis: for X being set st x in X holds
swap ({X},x,y) = {((X \ {x}) \/ {y})}
let X be set ; :: thesis: ( x in X implies swap ({X},x,y) = {((X \ {x}) \/ {y})} )
assume A1: x in X ; :: thesis: swap ({X},x,y) = {((X \ {x}) \/ {y})}
thus swap ({X},x,y) c= {((X \ {x}) \/ {y})} :: according to XBOOLE_0:def 10 :: thesis: {((X \ {x}) \/ {y})} c= swap ({X},x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in swap ({X},x,y) or a in {((X \ {x}) \/ {y})} )
assume a in swap ({X},x,y) ; :: thesis: a in {((X \ {x}) \/ {y})}

per cases then ( a in { ((A \ {x}) \/ {y}) where A is Element of {X} : x in A } or a in { (A \/ {x}) where A is Element of {X} : ( not x in A & A in {X} ) } ) by XBOOLE_0:def 3;

suppose a in { ((A \ {x}) \/ {y}) where A is Element of {X} : x in A } ; :: thesis: a in {((X \ {x}) \/ {y})}

then consider A being Element of {X} such that
A2: ( a = (A \ {x}) \/ {y} & x in A ) ;
A = X by TARSKI:def 1;
hence a in {((X \ {x}) \/ {y})} by A2, TARSKI:def 1; :: thesis: verum

end;

suppose a in { (A \/ {x}) where A is Element of {X} : ( not x in A & A in {X} ) } ; :: thesis: a in {((X \ {x}) \/ {y})}

then ex A being Element of {X} st
( a = A \/ {x} & not x in A & A in {X} ) ;
hence a in {((X \ {x}) \/ {y})} by A1, TARSKI:def 1; :: thesis: verum

end;

end;

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {((X \ {x}) \/ {y})} or a in swap ({X},x,y) )
assume a in {((X \ {x}) \/ {y})} ; :: thesis: a in swap ({X},x,y)
then ( a = (X \ {x}) \/ {y} & X in {X} ) by TARSKI:def 1;
then a in { ((A \ {x}) \/ {y}) where A is Element of {X} : x in A } by A1;
hence a in swap ({X},x,y) by XBOOLE_0:def 3; :: thesis: verum