let a, b be Nat; :: thesis: ( a,b are_coprime implies for n being non trivial Nat holds max ((a mod n),(b mod n)) > 0 )
assume A1: a,b are_coprime ; :: thesis: for n being non trivial Nat holds max ((a mod n),(b mod n)) > 0
assume not for n being non trivial Nat holds max ((a mod n),(b mod n)) > 0 ; :: thesis: contradiction
then consider m being non trivial Nat such that
A2: max ((a mod m),(b mod m)) <= 0 ;
( a mod m = 0 & b mod m = 0 ) by A2;
then ( m divides a & m divides b ) by INT_1:62;
hence contradiction by A1, PYTHTRIP:def 1, NAT_2:def 1; :: thesis: verum