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