let O be set ; :: thesis: for G being GroupWithOperators of O
for A being Subset of G st A is empty holds
the_stable_subgroup_of A = (1). G
let G be GroupWithOperators of O; :: thesis: for A being Subset of G st A is empty holds
the_stable_subgroup_of A = (1). G
let A be Subset of G; :: thesis: ( A is empty implies the_stable_subgroup_of A = (1). G )
A1: now :: thesis: for H being strict StableSubgroup of G st A c= the carrier of H holds
(1). G is StableSubgroup of H
let H be strict StableSubgroup of G; :: thesis: ( A c= the carrier of H implies (1). G is StableSubgroup of H )
assume A c= the carrier of H ; :: thesis: (1). G is StableSubgroup of H
(1). G = (1). H by Th15;
hence (1). G is StableSubgroup of H ; :: thesis: verum
end;
assume A is empty ; :: thesis: the_stable_subgroup_of A = (1). G
then A c= the carrier of ((1). G) ;
hence the_stable_subgroup_of A = (1). G by A1, Def26; :: thesis: verum