let n be Nat; :: thesis: (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3)
n >= 0 by NAT_1:2;
then A1: n + 1 > 0 by NAT_1:13;
then (n + 1) + 1 > 0 by NAT_1:13;
then (n + 2) + 1 > 0 by NAT_1:13;
then (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = ((1 * (n + 3)) / ((n + 1) * (n + 3))) - (2 / ((n + 1) * (n + 3))) by XCMPLX_1:91
.= ((n + 3) - 2) / ((n + 1) * (n + 3)) by XCMPLX_1:120
.= ((n + 1) * 1) / ((n + 1) * (n + 3))
.= 1 / (n + 3) by A1, XCMPLX_1:91 ;
hence (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3) ; :: thesis: verum