theorem :: GROUP_22:40
for G being non trivial Group st ex H being strict Subgroup of G st H is maximal holds
Phi G is characteristic Subgroup of G