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: G is Subgroup of G by GROUP_2:63;

now

let o be Element of O; :: thesis: G ^ o = (G ^ o) | the carrier of G
dom (G ^ o) c= the carrier of G ;
hence G ^ o = (G ^ o) | the carrier of G by RELAT_1:97; :: thesis: verum

end;

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