theorem :: XCMPLX_1:66

for a, b being Complex st a = (a + b) / 2 holds
a = b ;