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

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:68; :: thesis: verum

end;

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