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: for o being Element of O holds G ^ o = (G ^ o) | the carrier of G ;

G is Subgroup of G by GROUP_2:54;

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

let G be GroupWithOperators of O; :: thesis: G is StableSubgroup of G

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

G is Subgroup of G by GROUP_2:54;

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