defpred S₁[ set ] means ex y being set st
( y in X & $1 = {t,y} );
consider S being set such that
A1: for z being set holds
( z in S iff ( z in bool (X \/ {t}) & S₁[z] ) ) from XBOOLE_0:sch 1();
take S ; :: thesis: for z being set holds
( z in S iff ex y being set st
( y in X & z = {t,y} ) )
let z be set ; :: thesis: ( z in S iff ex y being set st
( y in X & z = {t,y} ) )
thus ( z in S implies S₁[z] ) by A1; :: thesis: ( ex y being set st
( y in X & z = {t,y} ) implies z in S )
assume A2: S₁[z] ; :: thesis: z in S
then consider y being set such that
A3: ( y in X & z = {t,y} ) ;
t in {t} by TARSKI:def 1;
then A4: t in X \/ {t} by XBOOLE_0:def 3;
y in X \/ {t} by A3, XBOOLE_0:def 3;
then z c= X \/ {t} by A3, A4, ZFMISC_1:38;
hence z in S by A1, A2; :: thesis: verum