let p be Safe Prime; :: thesis: ex q being Sophie_Germain Prime ex H1, H2, Hq, H2q being strict Subgroup of Z/Z* p st
( 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 ) ) )

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 ;
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 ;
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 ;
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: ex H1, H2, Hq, H2q being strict Subgroup of Z/Z* p st
( 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 ) ) )

take H1 ; :: thesis: ex H2, Hq, H2q being strict Subgroup of Z/Z* p st
( 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 ) ) )

take H2 ; :: thesis: ex Hq, H2q being strict Subgroup of Z/Z* p st
( 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 ) ) )

take Hq ; :: thesis: ex H2q being strict Subgroup of Z/Z* p st
( 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 ) ) )

take H2q ; :: thesis: ( 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 ) ) )

now :: thesis: for H being strict Subgroup of Z/Z* p holds
( H = H1 or H = H2 or H = Hq or H = H2q )
let H be strict Subgroup of Z/Z* p; :: thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
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 ;
A11: G1 = H by A10;
now :: thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
per cases ( card H = 1 or card H = 2 or card H = q or card H = 2 * q ) by ;
suppose card H = 1 ; :: thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A6, A10, A11; :: thesis: verum
end;
suppose card H = 2 ; :: thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A8, A10, A11; :: thesis: verum
end;
suppose card H = q ; :: thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A9, A10, A11; :: thesis: verum
end;
suppose card H = 2 * q ; :: thesis: ( H = H1 or H = H2 or H = Hq or H = H2q )
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) by A7, A10, A11; :: thesis: verum
end;
end;
end;
hence ( H = H1 or H = H2 or H = Hq or H = H2q ) ; :: thesis: verum
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: verum