hereby :: thesis: ( ex m, n being Element of NAT st
( m in X & n in X & m,n are_coprime ) 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_coprime )
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_coprime )
take b = b; :: thesis: ( a in X & b in X & a,b are_coprime )
thus a in X by A3, ENUMSET1:def 1; :: thesis: ( b in X & a,b are_coprime )
thus b in X by A3, ENUMSET1:def 1; :: thesis: a,b are_coprime

now :: thesis: for k being Nat st k divides a & k divides b holds
k = 1

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 Nat st n in X holds
k1 divides n by A3, A4, ENUMSET1:def 1;
hence k = 1 by A1; :: thesis: verum

end;

hence a,b are_coprime ; :: thesis: verum

end;

given m, n being Element of NAT such that A5: ( m in X & n in X ) and
A6: m,n are_coprime ; :: thesis: X is simplified
let k be Nat; :: according to PYTHTRIP:def 7 :: thesis: ( ( for n being Nat st n in X holds
k divides n ) implies k = 1 )
assume for n being 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;
then k divides 1 by A7, NAT_D:def 5;
hence k = 1 by WSIERP_1:15; :: thesis: verum