theorem Th11: :: RELSET_3:11

for z, z1, z2 being Complex
for X being complex-membered set holds
( [z1,z2] in addRel (X,z) iff ( z1 in X & z2 in X & z2 = z + z1 ) )