let X be non trivial set ; :: thesis: for x being Element of X ex y being set st
( y in X & x <> y )
let x be Element of X; :: thesis: ex y being set st
( y in X & x <> y )
ex y being set st
( y in X & y <> x )

proof

assume A1: for y being set holds
( not y in X or y = x ) ; :: thesis: contradiction
X c= {x}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in {x} )
assume z in X ; :: thesis: z in {x}
then z = x by A1;
hence z in {x} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

then consider y being set such that
A2: ( y in X & y <> x ) ;
take y ; :: thesis: ( y in X & x <> y )
thus ( y in X & x <> y ) by A2; :: thesis: verum