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

for H1 being StableSubgroup of G holds

( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds

( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

let H1 be StableSubgroup of G; :: thesis: ( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

A1: (1). G is StableSubgroup of H1 by Th16;

hence ((1). G) /\ H1 = (1). G by Lm21; :: thesis: H1 /\ ((1). G) = (1). G

thus H1 /\ ((1). G) = (1). G by A1, Lm21; :: thesis: verum

for H1 being StableSubgroup of G holds

( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds

( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

let H1 be StableSubgroup of G; :: thesis: ( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

A1: (1). G is StableSubgroup of H1 by Th16;

hence ((1). G) /\ H1 = (1). G by Lm21; :: thesis: H1 /\ ((1). G) = (1). G

thus H1 /\ ((1). G) = (1). G by A1, Lm21; :: thesis: verum