let x be object ; :: thesis: for X being set st X <> {x} & X <> {} holds
ex y being object st
( y in X & y <> x )
let X be set ; :: thesis: ( X <> {x} & X <> {} implies ex y being object st
( y in X & y <> x ) )
assume that
A1: X <> {x} and
A2: X <> {} ; :: thesis: ex y being object st
( y in X & y <> x )

per cases ( not x in X or x in X ) ;

suppose A3: not x in X ; :: thesis: ex y being object st
( y in X & y <> x )

consider y being object such that
A4: y in X by A2, XBOOLE_0:7;
take y ; :: thesis: ( y in X & y <> x )
thus ( y in X & y <> x ) by A3, A4; :: thesis: verum

end;

suppose A5: x in X ; :: thesis: ex y being object st
( y in X & y <> x )

consider y being object such that
A6: ( ( y in X & not y in {x} ) or ( y in {x} & not y in X ) ) by A1, TARSKI:2;
take y ; :: thesis: ( y in X & y <> x )
thus ( y in X & y <> x ) by A5, A6, TARSKI:def 1; :: thesis: verum

end;

end;