theorem :: ZFMISC_1:35

for x being object
for X being set st X <> {x} & X <> {} holds
ex y being object st
( y in X & y <> x ) by Lm12;