let X be non trivial set ; :: thesis: for p being set ex q being Element of X st q <> p
let p be set ; :: thesis: ex q being Element of X st q <> p
not X \ {p} is empty by REALSET1:3;
then consider q being set such that
A1: q in X \ {p} by XBOOLE_0:def 1;
reconsider q = q as Element of X by A1;
take q ; :: thesis: q <> p
thus q <> p by A1, ZFMISC_1:56; :: thesis: verum