theorem :: NUMBER03:58
for n being even Nat st n > 6 holds
ex p, q being Prime st
( n - p,n - q are_coprime & p = 3 & q = 5 )