consider x, y being object such that
A1: x in X and
A2: y in X and
A3: x <> y by ZFMISC_1:def 10;
take x ; :: according to ZFMISC_1:def 10 :: thesis: ex b₁ being object 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, A2, A3, XBOOLE_0:def 3; :: thesis: verum