let G be Group; :: thesis: for H1, H2 being Subgroup of G st H1 * H2 = the carrier of (H1 "\/" H2) holds
H1 * H2 = H2 * H1
let H1, H2 be Subgroup of G; :: thesis: ( H1 * H2 = the carrier of (H1 "\/" H2) implies H1 * H2 = H2 * H1 )
assume A1: H1 * H2 = the carrier of (H1 "\/" H2) ; :: thesis: H1 * H2 = H2 * H1
then A2: H2 * H1 c= H1 * H2 by Th62;
for x being Element of G st x in H1 * H2 holds
x in H2 * H1

proof

let x be Element of G; :: thesis: ( x in H1 * H2 implies x in H2 * H1 )
assume x in H1 * H2 ; :: thesis: x in H2 * H1
then x in H1 "\/" H2 by A1;
then x " in H1 "\/" H2 by GROUP_2:51;
then consider h1, h2 being Element of G such that
B2: ( x " = h1 * h2 & h1 in H1 & h2 in H2 ) by A1, GROUP_5:4;
B3: x = (x ") "
.= (h2 ") * (h1 ") by B2, GROUP_1:17 ;
( h2 " in H2 & h1 " in H1 ) by B2, GROUP_2:51;
hence x in H2 * H1 by B3, GROUP_5:4; :: thesis: verum

end;

then H1 * H2 c= H2 * H1 ;
hence H1 * H2 = H2 * H1 by A2, XBOOLE_0:def 10; :: thesis: verum