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
A1: 1_ H1 = 1_ G by Th4;
( (1). H1 is StableSubgroup of G & the carrier of ((1). H1) = {(1_ H1)} ) by Def8, Th11;
hence (1). G = (1). H1 by A1, Def8; :: thesis: verum