let a, b, c be positive Real; :: thesis: ((b * c) / a) * ((c * a) / b) = c ^2
((b * c) / a) * ((c * a) / b) = ((b * c) * (c * a)) / (a * b) by XCMPLX_1:76
.= ((c * c) * (a * b)) / (a * b)
.= (c * c) * ((a * b) / (a * b)) by XCMPLX_1:74
.= (c * c) * 1 by XCMPLX_1:60 ;
hence ((b * c) / a) * ((c * a) / b) = c ^2 ; :: thesis: verum