let a, b be non zero Nat; :: thesis: for p being prime Nat st a + b = p holds
a,b are_coprime
let p be prime Nat; :: thesis: ( a + b = p implies a,b are_coprime )
A1: a + b > a + 0 by XREAL_1:6;
assume A2: a + b = p ; :: thesis: a,b are_coprime
then a,p are_coprime by A1, NAT_D:7, NAT_6:6;
hence a,b are_coprime by A2, NEWTON02:45; :: thesis: verum