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_{1} being object st

( x in X \/ Y & b_{1} in X \/ Y & not x = b_{1} )

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

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

( x in X \/ Y & 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