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 )
set p9 = 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 T by A1;
take q ; :: thesis: ( q in X & q <> p )
thus ( q in X & q <> p ) by A1, ZFMISC_1:56; :: thesis: verum