let p be Safe Prime; :: thesis: ex q being Sophie_Germain Prime st Euler p = 2 * q
consider q being Sophie_Germain Prime such that
A1: p = (2 * q) + 1 by SGSP0;
Euler p = p - 1 by EULER_1:21;
hence ex q being Sophie_Germain Prime st Euler p = 2 * q by A1; :: thesis: verum