consider x, y being set such that
A1: ( x in X & y in X & x <> y ) by ZFMISC_1:def 10;
take x ; :: according to ZFMISC_1:def 10 :: thesis: ex b₁ being set st
( x in X \/ Y & b₁ in X \/ Y & not x = b₁ )
take y ; :: thesis: ( x in X \/ Y & y in X \/ Y & not x = y )
thus ( x in X \/ Y & y in X \/ Y & not x = y ) by A1, XBOOLE_0:def 3; :: thesis: verum