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