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

for H being StableSubgroup of G holds 1_ G in H

let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G holds 1_ G in H

let H be StableSubgroup of G; :: thesis: 1_ G in H

H is Subgroup of G by Def7;

hence 1_ G in H by GROUP_2:46; :: thesis: verum

for H being StableSubgroup of G holds 1_ G in H

let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G holds 1_ G in H

let H be StableSubgroup of G; :: thesis: 1_ G in H

H is Subgroup of G by Def7;

hence 1_ G in H by GROUP_2:46; :: thesis: verum