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 SF1;
A2: Z/Z* p is cyclic Group by INT_7:31;
Z/Z* p is strict Subgroup of Z/Z* p by GROUP_2:63;
then consider H2q being strict Subgroup of Z/Z* p such that
A3: card H2q = 2 * q by A1;
consider a being Element of (Z/Z* p) such that
A5: ( ord a = 2 & gr {a} is strict Subgroup of Z/Z* p ) by A1, A2, SF2;
consider b being Element of (Z/Z* p) such that
a5: ( ord b = q & gr {b} is strict Subgroup of Z/Z* p ) by A1, A2, SF2;
( card (gr {a}) = 2 & card (gr {b}) = q ) by a5, A5, GR_CY_1:27;
then consider H2, Hq being strict Subgroup of Z/Z* p such that
A6: ( card H2 = 2 & card Hq = q ) ;
card ((1). (Z/Z* p)) = 1 by GROUP_2:81;
then consider H1 being strict Subgroup of Z/Z* p such that
A7: card H1 = 1 ;

A8: now

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
A9: ( card G1 = card H & ( for G2 being strict Subgroup of Z/Z* p st card G2 = card H holds
G2 = G1 ) ) by A2, GROUP_2:178, A1, GR_CY_2:28;
A10: G1 = H by A9;

now

per cases ( card H = 1 or card H = 2 or card H = q or card H = 2 * q ) by INT_2:44, A1, GROUP_2:178, LMPQ;

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 A7, A9, A10; :: 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 A6, A9, A10; :: 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 A6, A9, A10; :: 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 A3, A9, A10; :: thesis: verum

end;

end;

end;

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

end;

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 ) ) )
thus ( 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 A3, A6, A7, A8; :: thesis: verum