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

proof

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

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

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

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

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

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

then consider B being Element of Y such that
A6: ( a = B \/ {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 & {y} misses B ) by ZFMISC_1:50;
then A = B by A6, A5, XBOOLE_1:71;
hence contradiction by A2, A7, XBOOLE_0:3; :: thesis: verum

end;

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

then ex B being Element of Y st
( a = B & not x in B & B in Y ) ;
hence contradiction by A5, ZFMISC_1:136; :: thesis: verum

end;

end;

end;

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

then consider A being Element of X such that
A8: ( a = A & not x in A & A in X ) ;

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

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

then ex B being Element of Y st
( a = B \/ {y} & x in B ) ;
hence contradiction by A8, ZFMISC_1:136; :: thesis: verum

end;

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

then ex B being Element of Y st
( a = B & not x in B & B in Y ) ;
hence contradiction by A2, A8, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

end;

end;

assume that
A9: Ext (X,x,y) misses Ext (Y,x,y) and
A10: X meets Y ; :: thesis: contradiction
consider a being object such that
A11: ( a in X & a in Y ) by A10, 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 \/ {y} in { (A \/ {y}) where A is Element of X : x in A } & a \/ {y} in { (A \/ {y}) where A is Element of Y : x in A } ) by A11;
then ( a \/ {y} in Ext (X,x,y) & a \/ {y} in Ext (Y,x,y) ) by XBOOLE_0:def 3;
hence contradiction by A9, XBOOLE_0:3; :: thesis: verum

end;

suppose not x in a ; :: thesis: contradiction

then ( a in { A where A is Element of X : ( not x in A & A in X ) } & a in { A where A is Element of Y : ( not x in A & A in Y ) } ) by A11;
then ( a in Ext (X,x,y) & a in Ext (Y,x,y) ) by XBOOLE_0:def 3;
hence contradiction by A9, XBOOLE_0:3; :: thesis: verum

end;

end;