let G be strict Group; :: thesis: for H being strict Subgroup of G
for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G
let H be strict Subgroup of G; :: thesis: for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G
let a be Element of G; :: thesis: ( H is maximal & not a in H implies gr ((carr H) \/ {a}) = G )
assume that
A1: H is maximal and
A2: not a in H ; :: thesis: gr ((carr H) \/ {a}) = G
a in {a} by TARSKI:def 1;
then ( carr H c= (carr H) \/ {a} & a in (carr H) \/ {a} ) by XBOOLE_0:def 3, XBOOLE_1:7;
then ( gr (carr H) is Subgroup of gr ((carr H) \/ {a}) & a in gr ((carr H) \/ {a}) ) by Th38, Th41;
then ( H is Subgroup of gr ((carr H) \/ {a}) & H <> gr ((carr H) \/ {a}) ) by A2, Th40;
hence gr ((carr H) \/ {a}) = G by A1, Def7; :: thesis: verum