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