theorem Th7: :: ZF_FUND1:7

for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
omega c= X