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
Ext (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 Ext (X,x,y) misses swap (Y,x,y) )
assume A1: ( x <> y & not y in union X & not y in union Y ) ; :: thesis: Ext (X,x,y) misses swap (Y,x,y)
assume Ext (X,x,y) meets swap (Y,x,y) ; :: thesis: contradiction
then consider a being object such that
A2: ( a in Ext (X,x,y) & a in swap (Y,x,y) ) by XBOOLE_0:3;
reconsider a = a as set by TARSKI:1;
( x in a iff not y in a ) by A2, A1, Th14;
hence contradiction by A2, A1, Th17; :: thesis: verum