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_A:1;
consider IT being set such that
A2: for Y being set holds
( Y in IT iff ( Y in M & S₁[Y] ) ) from XFAMILY:sch 1();
take IT ; :: thesis: for Z being set holds
( Z in IT iff Z c= X )
thus for Z being set holds
( Z in IT iff Z c= X ) by A2, A1; :: thesis: verum