let p be Safe Prime; :: thesis: ex q being Sophie_Germain Prime st card (Z/Z* p) = 2 * q

consider q being Sophie_Germain Prime such that

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

p - 1 = 2 * q by A1;

hence ex q being Sophie_Germain Prime st card (Z/Z* p) = 2 * q by INT_7:23; :: thesis: verum

consider q being Sophie_Germain Prime such that

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

p - 1 = 2 * q by A1;

hence ex q being Sophie_Germain Prime st card (Z/Z* p) = 2 * q by INT_7:23; :: thesis: verum