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 being ZF-formula st Diagram (H,E) in X holds
Diagram (('not' H),E) in X