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