theorem Th18: :: ZF_FUND1:18

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 v1, v2 being Element of VAR holds
( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X )