let G be Group; :: thesis: for H being strict Subgroup of G holds
( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
let H be strict Subgroup of G; :: thesis: ( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
1_ G in H by GROUP_2:46;
then 1_ G in carr H by STRUCT_0:def 5;
then {(1_ G)} c= carr H by ZFMISC_1:31;
then A1: ( carr ((1). G) = {(1_ G)} & {(1_ G)} \/ (carr H) = carr H ) by GROUP_2:def 7, XBOOLE_1:12;
hence ((1). G) "\/" H = H by Th31; :: thesis: H "\/" ((1). G) = H
thus H "\/" ((1). G) = H by A1, Th31; :: thesis: verum