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

A1: now :: thesis: for o being Element of O holds G ^ o = (G ^ o) | the carrier of G

let o be Element of O; :: thesis: G ^ o = (G ^ o) | the carrier of G
thus G ^ o = (G ^ o) | the carrier of G ; :: thesis: verum

end;

G is Subgroup of G by GROUP_2:54;
hence G is StableSubgroup of G by A1, Def7; :: thesis: verum