consider Z being set such that
A1: for x being object holds
( x in Z iff ex Y being set st
( x in Y & Y in X ) ) by TARSKI_0:4;
take Z ; :: thesis: for x being object holds
( x in Z iff ex Y being set st
( x in Y & Y in X ) )
thus for x being object holds
( x in Z iff ex Y being set st
( x in Y & Y in X ) ) by A1; :: thesis: verum