let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G = 1_ H1
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds 1_ G = 1_ H1
let H1 be StableSubgroup of G; :: thesis: 1_ G = 1_ H1
reconsider H19 = H1 as Subgroup of G by Def7;
1_ H1 = 1_ H19 ;
hence 1_ G = 1_ H1 by GROUP_2:44; :: thesis: verum