let a, b be positive Nat; :: thesis: ( a,b ! are_coprime implies a,b are_coprime )
assume A1: a,b ! are_coprime ; :: thesis: a,b are_coprime
b divides (b + 0) ! by Lm3;
hence a,b are_coprime by A1, WSIERP_1:15, NEWTON:57; :: thesis: verum