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

for H being strict StableSubgroup of G holds

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

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

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

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

1_ G in H by Lm17;

then 1_ G in carr H by STRUCT_0:def 5;

then {(1_ G)} c= carr H by ZFMISC_1:31;

then A1: {(1_ G)} \/ (carr H) = carr H by XBOOLE_1:12;

carr ((1). G) = {(1_ G)} by Def8;

hence ( ((1). G) "\/" H = H & H "\/" ((1). G) = H ) by A1, Th25; :: thesis: verum

for H being strict StableSubgroup of G holds

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

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

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

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

1_ G in H by Lm17;

then 1_ G in carr H by STRUCT_0:def 5;

then {(1_ G)} c= carr H by ZFMISC_1:31;

then A1: {(1_ G)} \/ (carr H) = carr H by XBOOLE_1:12;

carr ((1). G) = {(1_ G)} by Def8;

hence ( ((1). G) "\/" H = H & H "\/" ((1). G) = H ) by A1, Th25; :: thesis: verum