let T be non trivial set ; :: thesis: for X being non trivial Subset of T
for p being set ex q being Element of T st
( q in X & q <> p )
let X be non trivial Subset of T; :: thesis: for p being set ex q being Element of T st
( q in X & q <> p )
let p be set ; :: thesis: ex q being Element of T st
( q in X & 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;
q in T by A1, Lm1;
then reconsider q = q as Element of T by Def1;
take q ; :: thesis: ( q in X & q <> p )
thus ( q in X & q <> p ) by A1, ZFMISC_1:56; :: thesis: verum