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

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