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

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) by XBOOLE_1:2;
hence the_stable_subgroup_of A = (1). G by A1, Def29; :: thesis: verum