hereby :: thesis: ( ( for k being Nat st k divides m & k divides n holds
k = 1 ) implies m,n are_coprime )

assume m,n are_coprime ; :: thesis: for k being Nat st k divides m & k divides n holds
k = 1
then A1: m gcd n = 1 ;
let k be Nat; :: thesis: ( k divides m & k divides n implies k = 1 )
assume ( k divides m & k divides n ) ; :: thesis: k = 1
then k divides 1 by A1, NAT_D:def 5;
hence k = 1 by WSIERP_1:15; :: thesis: verum

end;

assume for k being Nat st k divides m & k divides n holds
k = 1 ; :: thesis: m,n are_coprime
then A2: for k being Nat st k divides m & k divides n holds
k divides 1 ;
( 1 divides m & 1 divides n ) by NAT_D:6;
hence m gcd n = 1 by A2, NAT_D:def 5; :: according to INT_2:def 3 :: thesis: verum