let X be non trivial set ; :: thesis: for x being Element of X ex y being object st
( y in X & x <> y )
let x be Element of X; :: thesis: ex y being object st
( y in X & x <> y )
consider d1, d2 being object such that
A1: ( d1 in X & d2 in X ) and
A2: d1 <> d2 by ZFMISC_1:def 10;
( x <> d1 or x <> d2 ) by A2;
hence ex y being object st
( y in X & x <> y ) by A1; :: thesis: verum