let x, y be object ; :: thesis: for X, Y being set holds swap ((X \/ Y),x,y) = (swap (X,x,y)) \/ (swap (Y,x,y))
let X, Y be set ; :: thesis: swap ((X \/ Y),x,y) = (swap (X,x,y)) \/ (swap (Y,x,y))
thus swap ((X \/ Y),x,y) c= (swap (X,x,y)) \/ (swap (Y,x,y)) :: according to XBOOLE_0:def 10 :: thesis: (swap (X,x,y)) \/ (swap (Y,x,y)) c= swap ((X \/ Y),x,y)

proof

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

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

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

then consider A being Element of X \/ Y such that
A1: ( a = (A \ {x}) \/ {y} & x in A ) ;
X \/ Y <> {} by A1, SUBSET_1:def 1;
then ( A in X or A in Y ) by XBOOLE_0:def 3;
then ( a in { ((A \ {x}) \/ {y}) where A is Element of X : x in A } or a in { ((A \ {x}) \/ {y}) where A is Element of Y : x in A } ) by A1;
then ( a in swap (X,x,y) or a in swap (Y,x,y) ) by XBOOLE_0:def 3;
hence a in (swap (X,x,y)) \/ (swap (Y,x,y)) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider A being Element of X \/ Y such that
A2: ( a = A \/ {x} & not x in A & A in X \/ Y ) ;
( A in X or A in Y ) by A2, XBOOLE_0:def 3;
then ( a in { (A \/ {x}) where A is Element of X : ( not x in A & A in X ) } or a in { (A \/ {x}) where A is Element of Y : ( not x in A & A in Y ) } ) by A2;
then ( a in swap (X,x,y) or a in swap (Y,x,y) ) by XBOOLE_0:def 3;
hence a in (swap (X,x,y)) \/ (swap (Y,x,y)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A3: swap (X,x,y) c= swap ((X \/ Y),x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in swap (X,x,y) or a in swap ((X \/ Y),x,y) )
assume a in swap (X,x,y) ; :: thesis: a in swap ((X \/ Y),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 swap ((X \/ Y),x,y)

then consider A being Element of X such that
A4: ( a = (A \ {x}) \/ {y} & x in A ) ;
X <> {} by A4, SUBSET_1:def 1;
then A in X \/ Y by XBOOLE_0:def 3;
then a in { ((A \ {x}) \/ {y}) where A is Element of X \/ Y : x in A } by A4;
hence a in swap ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider A being Element of X such that
A5: ( a = A \/ {x} & not x in A & A in X ) ;
A in X \/ Y by A5, XBOOLE_0:def 3;
then a in { (A \/ {x}) where A is Element of X \/ Y : ( not x in A & A in X \/ Y ) } by A5;
hence a in swap ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

swap (Y,x,y) c= swap ((X \/ Y),x,y)

proof

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

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

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

then consider A being Element of Y such that
A6: ( a = (A \ {x}) \/ {y} & x in A ) ;
Y <> {} by A6, SUBSET_1:def 1;
then A in X \/ Y by XBOOLE_0:def 3;
then a in { ((A \ {x}) \/ {y}) where A is Element of X \/ Y : x in A } by A6;
hence a in swap ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider A being Element of Y such that
A7: ( a = A \/ {x} & not x in A & A in Y ) ;
A in X \/ Y by A7, XBOOLE_0:def 3;
then a in { (A \/ {x}) where A is Element of X \/ Y : ( not x in A & A in X \/ Y ) } by A7;
hence a in swap ((X \/ Y),x,y) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence (swap (X,x,y)) \/ (swap (Y,x,y)) c= swap ((X \/ Y),x,y) by A3, XBOOLE_1:8; :: thesis: verum