let p, q, r be Prime; :: thesis: ( (p * (p + 1)) + (q * (q + 1)) = r * (r + 1) implies ( p = q & q = 2 & r = 3 ) )
assume (p * (p + 1)) + (q * (q + 1)) = r * (r + 1) ; :: thesis: ( p = q & q = 2 & r = 3 )

per cases then ( ( p = 2 & q = 2 & r = 3 ) or ( p = 5 & q = 3 & r = 6 ) or ( p = 3 & q = 5 & r = 6 ) ) by Th44;

suppose ( p = 2 & q = 2 & r = 3 ) ; :: thesis: ( p = q & q = 2 & r = 3 )

hence ( p = q & q = 2 & r = 3 ) ; :: thesis: verum

end;

suppose ( p = 5 & q = 3 & r = 6 ) ; :: thesis: ( p = q & q = 2 & r = 3 )

hence ( p = q & q = 2 & r = 3 ) by XPRIMES0:6; :: thesis: verum

end;

suppose ( p = 3 & q = 5 & r = 6 ) ; :: thesis: ( p = q & q = 2 & r = 3 )

hence ( p = q & q = 2 & r = 3 ) by XPRIMES0:6; :: thesis: verum

end;

end;