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