let x, y be object ; :: thesis: for X being set st not x in X holds
swap ({X},x,y) = {(X \/ {x})}
let X be set ; :: thesis: ( not x in X implies swap ({X},x,y) = {(X \/ {x})} )
assume A1: not x in X ; :: thesis: swap ({X},x,y) = {(X \/ {x})}
thus swap ({X},x,y) c= {(X \/ {x})} :: according to XBOOLE_0:def 10 :: thesis: {(X \/ {x})} 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})} )
assume a in swap ({X},x,y) ; :: thesis: a in {(X \/ {x})}

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})}

then ex A being Element of {X} st
( a = (A \ {x}) \/ {y} & x in A ) ;
hence a in {(X \/ {x})} by A1, 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})}

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

end;

end;

end;

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