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
gr (carr H) is Subgroup of gr ((carr H) \/ {a}) by Th32, XBOOLE_1:7;
then A3: H is Subgroup of gr ((carr H) \/ {a}) by Th31;
a in {a} by TARSKI:def 1;
then a in (carr H) \/ {a} by XBOOLE_0:def 3;
then H <> gr ((carr H) \/ {a}) by A2, Th29;
hence gr ((carr H) \/ {a}) = G by A1, A3; :: thesis: verum