let p be Safe Prime; :: thesis:
consider q being Sophie_Germain Prime such that
A1: card (Z/Z* p) = 2 * q by Th13;
A2: Z/Z* p is cyclic Group by INT_7:31;
then consider a being Element of (Z/Z* p) such that
A3: ord a = 2 and
gr {a} is strict Subgroup of Z/Z* p by A1, Th14;
consider b being Element of (Z/Z* p) such that
A4: ord b = q and
gr {b} is strict Subgroup of Z/Z* p by A1, A2, Th14;
A5: card (gr {b}) = q by A4, GR_CY_1:7;
card ((1). (Z/Z* p)) = 1 by GROUP_2:69;
then consider H1 being strict Subgroup of Z/Z* p such that
A6: card H1 = 1 ;
Z/Z* p is strict Subgroup of Z/Z* p by GROUP_2:54;
then consider H2q being strict Subgroup of Z/Z* p such that
A7: card H2q = 2 * q by A1;
card (gr {a}) = 2 by A3, GR_CY_1:7;
then consider H2, Hq being strict Subgroup of Z/Z* p such that
A8: card H2 = 2 and
A9: card Hq = q by A5;
take q ; :: thesis:
take H1 ; :: thesis:
take H2 ; :: thesis:
take Hq ; :: thesis:
take H2q ; :: thesis:

now :: thesis:

let H be strict Subgroup of Z/Z* p; :: thesis:
consider G1 being strict Subgroup of Z/Z* p such that
card G1 = card H and
A10: for G2 being strict Subgroup of Z/Z* p st card G2 = card H holds
G2 = G1 by A1, A2, GROUP_2:148, GR_CY_2:22;
A11: G1 = H by A10;

now :: thesis:

per cases by A1, Th1, GROUP_2:148, INT_2:28;

suppose card H = 1 ; :: thesis:

hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A6, A10, A11; :: thesis:

end;

suppose card H = 2 ; :: thesis:

hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A8, A10, A11; :: thesis:

end;

suppose card H = q ; :: thesis:

hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A9, A10, A11; :: thesis:

end;

suppose card H = 2 * q ; :: thesis:

hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A7, A10, A11; :: thesis:

end;

end;

end;

hence ( H = H1 or H = H2 or H = Hq or H = H2q ) ; :: thesis:

end;

hence ( card H1 = 1 & card H2 = 2 & card Hq = q & card H2q = 2 * q & ( for H being strict Subgroup of Z/Z* p holds
( H = H1 or H = H2 or H = Hq or H = H2q ) ) ) by A7, A8, A9, A6; :: thesis: