let a, b, c, d be Complex; :: thesis: ((a - c) / (b - c)) / ((a - d) / (b - d)) = ((c - a) / (c - b)) * ((d - b) / (d - a))
((a - c) / (b - c)) / ((a - d) / (b - d)) = (((- 1) * (c - a)) / ((- 1) * (c - b))) / (((- 1) * (d - a)) / ((- 1) * (d - b)))
.= ((c - a) / (c - b)) / (((- 1) * (d - a)) / ((- 1) * (d - b))) by XCMPLX_1:91
.= ((c - a) / (c - b)) / ((d - a) / (d - b)) by XCMPLX_1:91
.= ((c - a) / (c - b)) * ((d - b) / (d - a)) by XCMPLX_1:79 ;
hence ((a - c) / (b - c)) / ((a - d) / (b - d)) = ((c - a) / (c - b)) * ((d - b) / (d - a)) ; :: thesis: verum