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 and
A3: 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 A3, ENUMSET1:def 1; :: thesis: ( b in X & a,b are_relative_prime )
thus b in X by A3, ENUMSET1:def 1; :: thesis: a,b are_relative_prime

now

let k be Nat; :: thesis: ( k divides a & k divides b implies k = 1 )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume A4: ( k divides a & k divides b ) ; :: thesis: k = 1
then ( k1 ^2 divides a ^2 & k1 ^2 divides b ^2 ) by 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 A3, A4, 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
A5: ( m in X & n in X ) and
A6: m,n are_relative_prime ;
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 A7: ( k divides m & k divides n ) by A5;
m gcd n = 1 by A6, INT_2:def 3;
then k divides 1 by A7, NAT_D:def 5;
hence k = 1 by WSIERP_1:15; :: thesis: verum