let n be even Nat; :: thesis: ( n > 6 implies ex p, q being Prime st
( n - p,n - q are_coprime & p = 3 & q = 5 ) )
assume A1: n > 6 ; :: thesis: ex p, q being Prime st
( n - p,n - q are_coprime & p = 3 & q = 5 )
3 = (2 * 1) + 1 ;
then reconsider p = 3 as odd Prime by PEPIN:41;
5 = (2 * 2) + 1 ;
then reconsider q = 5 as odd Prime by PEPIN:59;
take p ; :: thesis: ex q being Prime st
( n - p,n - q are_coprime & p = 3 & q = 5 )
take q ; :: thesis: ( n - p,n - q are_coprime & p = 3 & q = 5 )
A2: (n - p) - (n - q) = 2 ;
( 6 - 3 < n - 3 & 6 - 5 < n - 5 ) by A1, XREAL_1:14;
hence ( n - p,n - q are_coprime & p = 3 & q = 5 ) by A2, Th31; :: thesis: verum