hereby :: thesis: ( ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) implies X is simplified )

assume A1: X is simplified ; :: thesis: ex a, b being Element of NAT st
( a in X & b in X & a,b are_relative_prime )
consider a, b, c being Element of NAT such that
A2: ( (a ^2 ) + (b ^2 ) = c ^2 & X = {a,b,c} ) by Def4;
take a = a; :: thesis: ex b being Element of NAT st
( a in X & b in X & a,b are_relative_prime )
take b = b; :: thesis: ( a in X & b in X & a,b are_relative_prime )
thus a in X by A2, ENUMSET1:def 1; :: thesis: ( b in X & a,b are_relative_prime )
thus b in X by A2, ENUMSET1:def 1; :: thesis: a,b are_relative_prime

now

let k be Nat; :: thesis: ( k divides a & k divides b implies k = 1 )
assume A3: ( k divides a & k divides b ) ; :: thesis: k = 1
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
( k1 ^2 divides a ^2 & k1 ^2 divides b ^2 ) by A3, Th6;
then k ^2 divides c ^2 by A2, NAT_D:8;
then k1 divides c by Th6;
then for n being Element of NAT st n in X holds
k1 divides n by A2, A3, ENUMSET1:def 1;
hence k = 1 by A1, Def7; :: thesis: verum

end;

hence a,b are_relative_prime by Def1; :: thesis: verum

end;

assume ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) ; :: thesis: X is simplified
then consider m, n being Element of NAT such that
A4: ( m in X & n in X & m,n are_relative_prime ) ;
A5: m gcd n = 1 by A4, INT_2:def 4;
let k be Element of NAT ; :: according to PYTHTRIP:def 7 :: thesis: ( ( for n being Element of NAT st n in X holds
k divides n ) implies k = 1 )
assume for n being Element of NAT st n in X holds
k divides n ; :: thesis: k = 1
then ( k divides m & k divides n ) by A4;
then k divides 1 by A5, NAT_D:def 5;
hence k = 1 by WSIERP_1:20; :: thesis: verum