t in {t} by TARSKI:def 1;
then A1: t in X \/ {t} by XBOOLE_0:def 3;
defpred S₁[ object ] means ex y being set st
( y in X & $1 = {t,y} );
consider S being set such that
A2: for z being object 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 A2; :: thesis: ( ex y being set st
( y in X & z = {t,y} ) implies z in S )
assume A3: S₁[z] ; :: thesis: z in S
then consider y being set such that
A4: y in X and
A5: z = {t,y} ;
y in X \/ {t} by A4, XBOOLE_0:def 3;
then z c= X \/ {t} by A5, A1, ZFMISC_1:32;
hence z in S by A2, A3; :: thesis: verum