(3 ^2) + (4 ^2) = 5 ^2 ;
then reconsider X = {3,4,5} as Pythagorean_triple by Def4;
3 gcd 4 = 3 gcd (4 - 3) by PREPOWER:97
.= 1 by WSIERP_1:8 ;
then A1: ( 4 in X & 3,4 are_coprime ) by ENUMSET1:def 1;
( not 0 in X & 3 in X ) by ENUMSET1:def 1;
hence {3,4,5} is non degenerate simplified Pythagorean_triple by A1, Def8, ORDINAL1:def 16; :: thesis: verum