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