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

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