let p be Safe Prime; :: thesis: ex q being Sophie_Germain Prime st p = (2 * q) + 1

consider q being Prime such that

A1: (2 * q) + 1 = p by Def1;

q is Sophie_Germain Prime by A1, Def2;

hence ex q being Sophie_Germain Prime st p = (2 * q) + 1 by A1; :: thesis: verum

consider q being Prime such that

A1: (2 * q) + 1 = p by Def1;

q is Sophie_Germain Prime by A1, Def2;

hence ex q being Sophie_Germain Prime st p = (2 * q) + 1 by A1; :: thesis: verum