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