theorem Th5: :: ZF_FUND1:5

for V being Universe
for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
A /\ B in X