let G be strict Group; :: thesis:
set A = { a where a is Element of G : not a is generating } ;
thus the carrier of (Phi G) c= { a where a is Element of G : not a is generating } :: according to XBOOLE_0:def 10 :: thesis:

defpred S₁[ set , set ] means ex H1, H2 being strict Subgroup of G st
( $1 = H1 & $2 = H2 & H1 is Subgroup of H2 );
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in the carrier of (Phi G) ; :: thesis:
then x in Phi G by STRUCT_0:def 5;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def 5;
assume not x in { a where a is Element of G : not a is generating } ; :: thesis:
then a is generating ;
then consider B being Subset of G such that
A2: gr B = G and
A3: gr (B \ {a}) <> G ;
set M = B \ {a};

assume A5: a in gr (B \ {a}) ; :: thesis:

now :: thesis:

let b be Element of G; :: thesis:
b in gr B by A2, STRUCT_0:def 5;
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
len I = len F and
A6: rng F c= B and
A7: b = Product (F |^ I) by Th28;
rng (F |^ I) c= carr (gr (B \ {a}))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (F |^ I) ; :: thesis:
then consider y being object such that
A8: y in dom (F |^ I) and
A9: (F |^ I) . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A8;
len (F |^ I) = len F by Def3;
then A10: y in dom F by A8, FINSEQ_3:29;
then A11: x = (F /. y) |^ (@ (I /. y)) by A9, Def3;

now :: thesis:

per cases ;

suppose F /. y = a ; :: thesis:

then x in gr (B \ {a}) by A5, A11, Th4;
hence x in carr (gr (B \ {a})) by STRUCT_0:def 5; :: thesis:

end;

suppose F /. y <> a ; :: thesis:

then A12: not F /. y in {a} by TARSKI:def 1;
( F /. y = F . y & F . y in rng F ) by A10, FUNCT_1:def 3, PARTFUN1:def 6;
then F /. y in B \ {a} by A6, A12, XBOOLE_0:def 5;
then x in gr (B \ {a}) by A11, Th4, Th29;
hence x in carr (gr (B \ {a})) by STRUCT_0:def 5; :: thesis:

end;

hence x in carr (gr (B \ {a})) ; :: thesis:

end;

hence b in gr (B \ {a}) by A7, Th18; :: thesis:

end;

hence contradiction by A3, GROUP_2:62; :: thesis:

end;

defpred S₂[ Subgroup of G] means ( B \ {a} c= carr $1 & not a in $1 );
consider X being set such that
A13: X c= Subgroups G and
A14: for H being strict Subgroup of G holds
( H in X iff S₂[H] ) from GROUP_4:sch 2();
B \ {a} c= carr (gr (B \ {a})) by Def4;
then reconsider X = X as non empty set by A14, A4;
A15: for x, y, z being Element of X st S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be Element of X; :: thesis:
given H1, H2 being strict Subgroup of G such that A16: x = H1 and
A17: ( y = H2 & H1 is Subgroup of H2 ) ; :: thesis:
given H3, H4 being strict Subgroup of G such that A18: y = H3 and
A19: z = H4 and
A20: H3 is Subgroup of H4 ; :: thesis:
H1 is Subgroup of H4 by A17, A18, A20, GROUP_2:56;
hence S₁[x,z] by A16, A19; :: thesis:

end;

A21: for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S₁[x,y] holds
S₁[y,x] ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
S₁[x,y]

proof

let Y be set ; :: thesis:
assume A22: Y c= X ; :: thesis:
set C = { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } ;

now :: thesis:

let Z be set ; :: thesis:
assume Z in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } ; :: thesis:
then ex D being Subset of G st
( Z = D & ex H being strict Subgroup of G st
( H in Y & D = carr H ) ) ;
hence Z c= the carrier of G ; :: thesis:

end;

then reconsider E = union { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } as Subset of G by ZFMISC_1:76;
assume A23: for x, y being Element of X st x in Y & y in Y & not S₁[x,y] holds
S₁[y,x] ; :: thesis:

now :: thesis:

per cases ;

suppose A24: Y = {} ; :: thesis:

set y = the Element of X;
take y = the Element of X; :: thesis:
let x be Element of X; :: thesis:
assume x in Y ; :: thesis:
hence S₁[x,y] by A24; :: thesis:

end;

suppose A25: Y <> {} ; :: thesis:

A26: now :: thesis:

let a, b be Element of G; :: thesis:
assume that
A27: a in E and
A28: b in E ; :: thesis:
consider Z being set such that
A29: a in Z and
A30: Z in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } by A27, TARSKI:def 4;
consider Z1 being set such that
A31: b in Z1 and
A32: Z1 in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } by A28, TARSKI:def 4;
consider D being Subset of G such that
A33: Z = D and
A34: ex H being strict Subgroup of G st
( H in Y & D = carr H ) by A30;
consider B being Subset of G such that
A35: Z1 = B and
A36: ex H being strict Subgroup of G st
( H in Y & B = carr H ) by A32;
consider H1 being Subgroup of G such that
A37: H1 in Y and
A38: D = carr H1 by A34;
consider H2 being Subgroup of G such that
A39: H2 in Y and
A40: B = carr H2 by A36;

now :: thesis:

per cases by A22, A23, A37, A39;

suppose S₁[H1,H2] ; :: thesis:

then carr H1 c= the carrier of H2 by GROUP_2:def 5;
then a * b in carr H2 by A29, A33, A38, A31, A35, A40, GROUP_2:74;
hence a * b in E by A32, A35, A40, TARSKI:def 4; :: thesis:

end;

suppose S₁[H2,H1] ; :: thesis:

then carr H2 c= the carrier of H1 by GROUP_2:def 5;
then a * b in carr H1 by A29, A33, A38, A31, A35, A40, GROUP_2:74;
hence a * b in E by A30, A33, A38, TARSKI:def 4; :: thesis:

end;

hence a * b in E ; :: thesis:

end;

A41: now :: thesis:

let a be Element of G; :: thesis:
assume a in E ; :: thesis:
then consider Z being set such that
A42: a in Z and
A43: Z in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } by TARSKI:def 4;
consider D being Subset of G such that
A44: Z = D and
A45: ex H being strict Subgroup of G st
( H in Y & D = carr H ) by A43;
consider H1 being Subgroup of G such that
H1 in Y and
A46: D = carr H1 by A45;
a " in carr H1 by A42, A44, A46, GROUP_2:75;
hence a " in E by A43, A44, A46, TARSKI:def 4; :: thesis:

end;

set s = the Element of Y;
A47: the Element of Y in X by A22, A25;
then reconsider s = the Element of Y as strict Subgroup of G by A13, GROUP_3:def 1;
A48: carr s in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } by A25;
then A49: carr s c= E by ZFMISC_1:74;
E <> {} by A48, ORDERS_1:6;
then consider H being strict Subgroup of G such that
A50: the carrier of H = E by A26, A41, GROUP_2:52;

A51: now :: thesis:

assume a in H ; :: thesis:
then a in E by A50, STRUCT_0:def 5;
then consider Z being set such that
A52: a in Z and
A53: Z in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } by TARSKI:def 4;
consider D being Subset of G such that
A54: Z = D and
A55: ex H being strict Subgroup of G st
( H in Y & D = carr H ) by A53;
consider H1 being strict Subgroup of G such that
A56: H1 in Y and
A57: D = carr H1 by A55;
not a in H1 by A14, A22, A56;
hence contradiction by A52, A54, A57, STRUCT_0:def 5; :: thesis:

end;

B \ {a} c= carr s by A14, A47;
then A58: B \ {a} c= E by A49;
the carrier of H = carr H ;
then reconsider y = H as Element of X by A14, A58, A50, A51;
take y = y; :: thesis:
let x be Element of X; :: thesis:
assume A59: x in Y ; :: thesis:
x in Subgroups G by A13;
then reconsider K = x as strict Subgroup of G by GROUP_3:def 1;
take K = K; :: thesis:
take H = H; :: thesis:
thus ( x = K & y = H ) ; :: thesis:
carr K = the carrier of K ;
then the carrier of K in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } by A59;
hence K is Subgroup of H by A50, GROUP_2:57, ZFMISC_1:74; :: thesis:

end;

hence ex y being Element of X st
for x being Element of X st x in Y holds
S₁[x,y] ; :: thesis:

end;

A60: now :: thesis:

let x be Element of X; :: thesis:
x in Subgroups G by A13;
hence x is strict Subgroup of G by GROUP_3:def 1; :: thesis:

end;

A61: for x being Element of X holds S₁[x,x]

proof

let x be Element of X; :: thesis:
reconsider H = x as strict Subgroup of G by A60;
H is Subgroup of H by GROUP_2:54;
hence S₁[x,x] ; :: thesis:

end;

A62: for x, y being Element of X st S₁[x,y] & S₁[y,x] holds
x = y by GROUP_2:55;
consider s being Element of X such that
A63: for y being Element of X st s <> y holds
not S₁[s,y] from ORDERS_1:sch 1(A61, A62, A15, A21);
reconsider H = s as strict Subgroup of G by A60;
H is maximal

proof

not a in H by A14;
hence multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) by STRUCT_0:def 5; :: according to GROUP_4:def 6 :: thesis:
let K be strict Subgroup of G; :: thesis:
assume that
A64: K <> multMagma(# the carrier of H, the multF of H #) and
A65: H is Subgroup of K and
A66: K <> multMagma(# the carrier of G, the multF of G #) ; :: thesis:
A67: B \ {a} c= carr H by A14;
the carrier of H c= the carrier of K by A65, GROUP_2:def 5;
then A68: B \ {a} c= carr K by A67;

now :: thesis:

A69: B c= (B \ {a}) \/ {a}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A70: x in B ; :: thesis:

now :: thesis:

per cases ;

suppose x = a ; :: thesis:

then x in {a} by TARSKI:def 1;
hence x in (B \ {a}) \/ {a} by XBOOLE_0:def 3; :: thesis:

end;

suppose x <> a ; :: thesis:

then not x in {a} by TARSKI:def 1;
then x in B \ {a} by A70, XBOOLE_0:def 5;
hence x in (B \ {a}) \/ {a} by XBOOLE_0:def 3; :: thesis:

end;

hence x in (B \ {a}) \/ {a} ; :: thesis:

end;

assume a in K ; :: thesis:
then a in carr K by STRUCT_0:def 5;
then {a} c= carr K by ZFMISC_1:31;
then (B \ {a}) \/ {a} c= carr K by A68, XBOOLE_1:8;
then gr B is Subgroup of gr (carr K) by A69, Th32, XBOOLE_1:1;
then G is Subgroup of K by A2, Th31;
hence contradiction by A66, GROUP_2:55; :: thesis:

end;

then reconsider v = K as Element of X by A14, A68;
not S₁[s,v] by A63, A64;
hence contradiction by A65; :: thesis:

end;

then Phi G is Subgroup of H by Th40;
then the carrier of (Phi G) c= the carrier of H by GROUP_2:def 5;
then x in H by A1, STRUCT_0:def 5;
hence contradiction by A14; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { a where a is Element of G : not a is generating } ; :: thesis:
then consider a being Element of G such that
A71: x = a and
A72: not a is generating ;

now :: thesis:

per cases ;

suppose for H being strict Subgroup of G holds not H is maximal ; :: thesis:

then Phi G = G by Def7;
hence x in the carrier of (Phi G) by A71; :: thesis:

end;

suppose A73: ex H being strict Subgroup of G st H is maximal ; :: thesis:

now :: thesis:

let H be strict Subgroup of G; :: thesis:
assume A74: H is maximal ; :: thesis:

now :: thesis:

assume A75: not a in H ; :: thesis:
(carr H) /\ {a} c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A76: x in (carr H) /\ {a} ; :: thesis:
then x in {a} by XBOOLE_0:def 4;
then A77: x = a by TARSKI:def 1;
x in carr H by A76, XBOOLE_0:def 4;
hence x in {} by A75, A77, STRUCT_0:def 5; :: thesis:

end;

then (carr H) /\ {a} = {} ;
then A78: carr H misses {a} ;
((carr H) \/ {a}) \ {a} = (carr H) \ {a} by XBOOLE_1:40
.= carr H by A78, XBOOLE_1:83 ;
then A79: gr (((carr H) \/ {a}) \ {a}) = H by Th31;
A80: H <> G by A74;
gr ((carr H) \/ {a}) = G by A74, A75, Th37;
hence contradiction by A72, A79, A80; :: thesis:

end;

hence a in H ; :: thesis:

end;

then a in Phi G by A73, Th38;
hence x in the carrier of (Phi G) by A71, STRUCT_0:def 5; :: thesis:

end;

hence x in the carrier of (Phi G) ; :: thesis: