consider M being set such that
A1: ( X in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) ) and
for X being set st X in M holds
ex Z being set st
( Z in M & ( for Y being set st Y c= X holds
Y in Z ) ) and
for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by TARSKI:9;
consider IT being set such that
A2: for Y being set holds
( Y in IT iff ( Y in M & S₁[Y] ) ) from XBOOLE_0:sch 1();
take IT ; :: thesis: for Z being set holds
( Z in IT iff Z c= X )
let Y be set ; :: thesis: ( Y in IT iff Y c= X )
thus ( Y in IT implies Y c= X ) by A2; :: thesis: ( Y c= X implies Y in IT )
assume A3: Y c= X ; :: thesis: Y in IT
then Y in M by A1;
hence Y in IT by A2, A3; :: thesis: verum