let r, s, t be Real; :: thesis: ( not r is zero & not s is zero & not t is zero implies (((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = 1 )
assume that
A1: not r is zero and
A2: not s is zero and
A3: not t is zero ; :: thesis: (((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = 1
(((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = ((r / s) * ((- t) / (- r))) * ((- s) / (- t)) by XCMPLX_1:191
.= ((r / s) * (t / r)) * ((- s) / (- t)) by XCMPLX_1:191
.= ((r / s) * (t / r)) * (s / t) by XCMPLX_1:191
.= ((((r / r) * s) / s) * t) / t
.= (((1 * s) / s) * t) / t by A1, XCMPLX_1:60
.= ((1 * 1) * t) / t by A2, XCMPLX_1:60
.= (1 * 1) * 1 by A3, XCMPLX_1:60 ;
hence (((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = 1 ; :: thesis: verum