theorem :: TARSKI_0:4

for X being set ex Z being set st
for x being object holds
( x in Z iff ex Y being set st
( x in Y & Y in X ) ) ;