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

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

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

then ex A being Element of X st
( Y = A \/ {y} & x in A ) ;
hence ( x in Y iff y in Y ) by ZFMISC_1:136; :: thesis: verum

end;

suppose Y in { A where A is Element of X : ( not x in A & A in X ) } ; :: thesis: ( x in Y iff y in Y )

then ex A being Element of X st
( Y = A & not x in A & A in X ) ;
hence ( x in Y iff y in Y ) by A2, TARSKI:def 4; :: thesis: verum

end;

end;