theorem Th3: :: ZF_FUND1:3

for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
{} in X