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