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 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: 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 ) ) )

( H = H1 or H = H2 or H = Hq or H = H2q ) ) ) by A7, A8, A9, A6; :: thesis: verum

( 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 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: 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 )

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 )

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 A1, A2, GROUP_2:148, GR_CY_2:22;

A11: G1 = H by A10;

end;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: ( H = H1 or H = H2 or H = Hq or H = H2q )end;

hence
( H = H1 or H = H2 or H = Hq or H = H2q )
; :: thesis: verumper cases
( card H = 1 or card H = 2 or card H = q or card H = 2 * q )
by A1, Th1, GROUP_2:148, INT_2:28;

end;

( H = H1 or H = H2 or H = Hq or H = H2q ) ) ) by A7, A8, A9, A6; :: thesis: verum