let n be Nat; :: thesis: 1 / (Triangle n) = 2 / (n * (n + 1))
1 / (Triangle n) = 1 / ((n * (n + 1)) / 2) by Th19
.= 2 / (n * (n + 1)) by XCMPLX_1:57 ;
hence 1 / (Triangle n) = 2 / (n * (n + 1)) ; :: thesis: verum