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 ; :: thesis: ( b in X & a,b are_coprime )
thus b in X by ; :: 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 ;
then k1 divides c by Th6;
then for n being Element of NAT st n in X holds
k1 divides n by ;
hence k = 1 by A1; :: thesis: verum
end;
hence a,b are_coprime ; :: thesis: verum
end;
assume ex m, n being Element of NAT st
( m in X & n in X & m,n are_coprime ) ; :: 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_coprime ;
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;
then k divides 1 by ;
hence k = 1 by WSIERP_1:15; :: thesis: verum