let G be Group; :: thesis: for a being Element of G st ( for H being strict Subgroup of G holds not H is maximal ) holds
a in Phi G
let a be Element of G; :: thesis: ( ( for H being strict Subgroup of G holds not H is maximal ) implies a in Phi G )
assume for H being strict Subgroup of G holds not H is maximal ; :: thesis: a in Phi G
then Phi G = multMagma(# the carrier of G, the multF of G #) by Def7;
hence a in Phi G by STRUCT_0:def 5; :: thesis: verum