let p be Safe Prime; :: thesis: ex q being Sophie_Germain Prime st Euler p = 2 * q
A1: Euler p = p - 1 by EULER_1:20;
ex q being Sophie_Germain Prime st p = (2 * q) + 1 by Th10;
hence ex q being Sophie_Germain Prime st Euler p = 2 * q by A1; :: thesis: verum