let t be 1 _greater Nat; :: thesis: ( t > 0 & t > 1 & t " > 0 & t * (t ") = 1 )
t is 1 _greater ;
hence ( t > 0 & t > 1 & t " > 0 & t * (t ") = 1 ) by XCMPLX_0:def 7; :: thesis: verum