let r be Real; :: thesis: ( tan r = (cot r) " & cot r = (tan r) " )
thus tan r = (((sin r) * ((cos r) ")) ") "
.= (((sin r) ") * (((cos r) ") ")) " by XCMPLX_1:204
.= (cot r) " ; :: thesis: cot r = (tan r) "
thus cot r = (((cos r) * ((sin r) ")) ") "
.= (((cos r) ") * (((sin r) ") ")) " by XCMPLX_1:204
.= (tan r) " ; :: thesis: verum