let G be Group; :: thesis: for H being strict Subgroup of G st H is maximal holds
Phi G is Subgroup of H
let H be strict Subgroup of G; :: thesis: ( H is maximal implies Phi G is Subgroup of H )
assume H is maximal ; :: thesis: Phi G is Subgroup of H
then for a being Element of G st a in Phi G holds
a in H by Th38;
hence Phi G is Subgroup of H by GROUP_2:58; :: thesis: verum