let x, y be object ; :: thesis: for X, Y being set st x <> y & not y in union X & not y in union Y holds
( X misses Y iff swap (X,x,y) misses swap (Y,x,y) )
let X, Y be set ; :: thesis: ( x <> y & not y in union X & not y in union Y implies ( X misses Y iff swap (X,x,y) misses swap (Y,x,y) ) )
assume A1: ( x <> y & not y in union X & not y in union Y ) ; :: thesis: ( X misses Y iff swap (X,x,y) misses swap (Y,x,y) )
thus ( X misses Y implies swap (X,x,y) misses swap (Y,x,y) ) :: thesis: ( swap (X,x,y) misses swap (Y,x,y) implies X misses Y )

proof

assume that
A2: X misses Y and
A3: swap (X,x,y) meets swap (Y,x,y) ; :: thesis: contradiction
consider a being object such that
A4: ( a in swap (X,x,y) & a in swap (Y,x,y) ) by XBOOLE_0:3, A3;

per cases ( 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 A4, XBOOLE_0:def 3;

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

then consider A being Element of X such that
A5: ( a = (A \ {x}) \/ {y} & x in A ) ;

per cases ( 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 A4, XBOOLE_0:def 3;

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

then consider B being Element of Y such that
A6: ( a = (B \ {x}) \/ {y} & x in B ) ;
A7: ( X <> {} & Y <> {} ) by A5, A6, SUBSET_1:def 1;
then ( not y in A & not y in B ) by A1, TARSKI:def 4;
then ( {y} misses A \ {x} & {y} misses B \ {x} ) by XBOOLE_1:80, ZFMISC_1:50;
then ( A = (A \ {x}) \/ {x} & (A \ {x}) \/ {x} = (B \ {x}) \/ {x} & (B \ {x}) \/ {x} = B ) by A6, A5, ZFMISC_1:116, XBOOLE_1:71;
hence contradiction by A2, A7, XBOOLE_0:3; :: thesis: verum

end;

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

then consider B being Element of Y such that
A8: ( a = B \/ {x} & not x in B & B in Y ) ;
not x in A \ {x} by ZFMISC_1:56;
then not x in (A \ {x}) \/ {y} by ZFMISC_1:136, A1;
hence contradiction by A5, A8, ZFMISC_1:136; :: thesis: verum

end;

end;

end;

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

then consider A being Element of X such that
A9: ( a = A \/ {x} & not x in A & A in X ) ;

per cases ( 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 A4, XBOOLE_0:def 3;

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

then consider B being Element of Y such that
A10: ( a = (B \ {x}) \/ {y} & x in B ) ;
not x in B \ {x} by ZFMISC_1:56;
then not x in (B \ {x}) \/ {y} by ZFMISC_1:136, A1;
hence contradiction by A9, A10, ZFMISC_1:136; :: thesis: verum

end;

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

then consider B being Element of Y such that
A11: ( a = B \/ {x} & not x in B & B in Y ) ;
( {x} misses A & {x} misses B ) by A9, A11, ZFMISC_1:50;
then A = B by A11, A9, XBOOLE_1:71;
hence contradiction by A2, A9, A11, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

end;

end;

assume that
A12: swap (X,x,y) misses swap (Y,x,y) and
A13: X meets Y ; :: thesis: contradiction
consider a being object such that
A14: ( a in X & a in Y ) by A13, XBOOLE_0:3;
reconsider a = a as set by TARSKI:1;

per cases ( x in a or not x in a ) ;

suppose x in a ; :: thesis: contradiction

then ( (a \ {x}) \/ {y} in { ((A \ {x}) \/ {y}) where A is Element of X : x in A } & (a \ {x}) \/ {y} in { ((A \ {x}) \/ {y}) where A is Element of Y : x in A } ) by A14;
then ( (a \ {x}) \/ {y} in swap (X,x,y) & (a \ {x}) \/ {y} in swap (Y,x,y) ) by XBOOLE_0:def 3;
hence contradiction by A12, XBOOLE_0:3; :: thesis: verum

end;

suppose not x in a ; :: thesis: contradiction

then ( a \/ {x} in { (A \/ {x}) where A is Element of X : ( not x in A & A in X ) } & a \/ {x} in { (A \/ {x}) where A is Element of Y : ( not x in A & A in Y ) } ) by A14;
then ( a \/ {x} in swap (X,x,y) & a \/ {x} in swap (Y,x,y) ) by XBOOLE_0:def 3;
hence contradiction by A12, XBOOLE_0:3; :: thesis: verum

end;

end;