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 ZFMISC_1:139;
then consider q being object such that
A1: q in X \ {p} ;
reconsider q = q as set by TARSKI:1;
X \ {p} c= X by XBOOLE_1:36;
then q in X by A1;
then reconsider q = q as Element of X by Def1;
take q ; :: thesis: q <> p
thus q <> p by A1, ZFMISC_1:56; :: thesis: verum