let G be non trivial Group; :: thesis: ( ex H being strict Subgroup of G st H is maximal implies Phi G is characteristic Subgroup of G )
defpred S₁[ Subgroup of G] means $1 is maximal ;
assume A1: ex H being strict Subgroup of G st S₁[H] ; :: thesis: Phi G is characteristic Subgroup of G
set MaxSubCarrs = { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & S₁[H] ) } ;
A2: for phi being Automorphism of G
for H being strict Subgroup of G st S₁[H] holds
S₁[ Image (phi | H)] by Th24;
consider K being strict Subgroup of G such that
A3: the carrier of K = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & S₁[H] ) } and
A4: K is characteristic from GROUP_22:sch 2(A2, A1);
thus Phi G is characteristic Subgroup of G by A4, A1, A3, GROUP_4:def 7; :: thesis: verum