reconsider n0 = Triangle n as non zero Nat by TARSKI:1;
consider p being Nat such that
A1: n = Mersenne p by Def12;
2 to_power p > 0 by POWER:34;
then 2 |^ p >= 0 + 1 by NAT_1:13;
then A2: (2 |^ p) -' 1 = (2 |^ p) - 1 by XREAL_0:def 2, XREAL_1:19;
A3: p -' 1 = p - 1 by XREAL_1:233, A1, GR_CY_3:16, NAT_1:14;
reconsider p1 = Mersenne p as Nat ;
(2 to_power p) / (2 to_power 1) = (p1 + 1) / 2 ;
then 2 to_power (p -' 1) = (p1 + 1) / 2 by A3, POWER:29;
then p1 * (2 |^ (p -' 1)) = (p1 * (p1 + 1)) / 2 ;
then n0 is perfect by NAT_5:38, A2, A1, Th19;
hence Triangle n is perfect ; :: thesis: verum