reconsider p = 127 as Prime by XPRIMES1:127;
reconsider q = 3697 as Prime by XPRIMES1:3697;
reconsider r = 5227 as Prime by XPRIMES1:5227;
take p ; :: thesis: ex q, r being Prime st Triangle p, Triangle q, Triangle r form_an_AP
take q ; :: thesis: ex r being Prime st Triangle p, Triangle q, Triangle r form_an_AP
take r ; :: thesis: Triangle p, Triangle q, Triangle r form_an_AP
T1: Triangle 127 = (127 * (127 + 1)) / 2 by NUMPOLY1:19
.= 8128 ;
T2: Triangle 3697 = (3697 * (3697 + 1)) / 2 by NUMPOLY1:19
.= 6835753 ;
Triangle 5227 = (5227 * (5227 + 1)) / 2 by NUMPOLY1:19
.= 13663378 ;
then (Triangle 5227) - (Triangle 3697) = (Triangle 3697) - (Triangle 127) by T1, T2;
hence Triangle p, Triangle q, Triangle r form_an_AP by NUMBER06:def 9; :: thesis: verum