let O be set ; :: thesis: for G being GroupWithOperators of O

for H being strict StableSubgroup of G holds the_stable_subgroup_of (carr H) = H

let G be GroupWithOperators of O; :: thesis: for H being strict StableSubgroup of G holds the_stable_subgroup_of (carr H) = H

let H be strict StableSubgroup of G; :: thesis: the_stable_subgroup_of (carr H) = H

for H1 being strict StableSubgroup of G st carr H c= the carrier of H1 holds

H is StableSubgroup of H1 by Lm20;

hence the_stable_subgroup_of (carr H) = H by Def26; :: thesis: verum

for H being strict StableSubgroup of G holds the_stable_subgroup_of (carr H) = H

let G be GroupWithOperators of O; :: thesis: for H being strict StableSubgroup of G holds the_stable_subgroup_of (carr H) = H

let H be strict StableSubgroup of G; :: thesis: the_stable_subgroup_of (carr H) = H

for H1 being strict StableSubgroup of G st carr H c= the carrier of H1 holds

H is StableSubgroup of H1 by Lm20;

hence the_stable_subgroup_of (carr H) = H by Def26; :: thesis: verum