(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

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