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 )

then A c= the carrier of ((1). G) ;

hence the_stable_subgroup_of A = (1). G by A1, Def26; :: thesis: verum

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

assume
A is empty
; :: thesis: the_stable_subgroup_of A = (1). G(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 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

then A c= the carrier of ((1). G) ;

hence the_stable_subgroup_of A = (1). G by A1, Def26; :: thesis: verum