let I be non trivial set ; :: thesis: ex i, j being Element of I st i <> j

ex x, y being object st

( x in I & y in I & x <> y ) by ZFMISC_1:def 10;

hence ex i, j being Element of I st i <> j ; :: thesis: verum

ex x, y being object st

( x in I & y in I & x <> y ) by ZFMISC_1:def 10;

hence ex i, j being Element of I st i <> j ; :: thesis: verum