theorem Th20: :: ZF_FUND1:20

for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds
Diagram ((H '&' H9),E) in X