let G be strict Group; :: thesis: for x, y being Element of G
for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
let x, y be Element of G; :: thesis: for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
let H, K be strict Subgroup of G; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )

per cases ( for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) or ex z being Element of G st
( z in (H * x) * K & z in (H * y) * K ) ) ;

suppose for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) ; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )

hence ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) ) ; :: thesis: verum

end;

suppose ex z being Element of G st
( z in (H * x) * K & z in (H * y) * K ) ; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )

then consider z being Element of G such that
A1: z in (H * x) * K and
A2: z in (H * y) * K ;
consider h1, k1 being Element of G such that
A3: z = (h1 * x) * k1 and
A4: h1 in H and
A5: k1 in K by A1, Th17;
consider h2, k2 being Element of G such that
A6: z = (h2 * y) * k2 and
A7: h2 in H and
A8: k2 in K by A2, Th17;
for a being object st a in (H * x) * K holds
a in (H * y) * K

proof

let a be object ; :: thesis: ( a in (H * x) * K implies a in (H * y) * K )
assume a in (H * x) * K ; :: thesis: a in (H * y) * K
then consider h, k being Element of G such that
A9: a = (h * x) * k and
A10: h in H and
A11: k in K by Th17;
ex c, d being Element of G st
( a = (c * y) * d & c in H & d in K )

proof

h = h * (1_ G) by GROUP_1:def 4;
then A12: (h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k by GROUP_1:def 4;
1_ G = (h1 ") * h1 by GROUP_1:def 5;
then A13: (h * x) * k = (((h * ((h1 ") * h1)) * x) * (k1 * (k1 "))) * k by A12, GROUP_1:def 5
.= ((((h * ((h1 ") * h1)) * x) * k1) * (k1 ")) * k by GROUP_1:def 3
.= (((((h * (h1 ")) * h1) * x) * k1) * (k1 ")) * k by GROUP_1:def 3
.= ((((h * (h1 ")) * (h1 * x)) * k1) * (k1 ")) * k by GROUP_1:def 3
.= (((h * (h1 ")) * ((h2 * y) * k2)) * (k1 ")) * k by A3, A6, GROUP_1:def 3
.= ((((h * (h1 ")) * (h2 * y)) * k2) * (k1 ")) * k by GROUP_1:def 3
.= (((((h * (h1 ")) * h2) * y) * k2) * (k1 ")) * k by GROUP_1:def 3
.= ((((h * (h1 ")) * h2) * y) * (k2 * (k1 "))) * k by GROUP_1:def 3
.= (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) by GROUP_1:def 3 ;
take (h * (h1 ")) * h2 ; :: thesis: ex d being Element of G st
( a = (((h * (h1 ")) * h2) * y) * d & (h * (h1 ")) * h2 in H & d in K )
take (k2 * (k1 ")) * k ; :: thesis: ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K )
h1 " in H by A4, GROUP_2:51;
then A14: h * (h1 ") in H by A10, GROUP_2:50;
k1 " in K by A5, GROUP_2:51;
then k2 * (k1 ") in K by A8, GROUP_2:50;
hence ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K ) by A7, A9, A11, A13, A14, GROUP_2:50; :: thesis: verum

end;

hence a in (H * y) * K by Th17; :: thesis: verum

end;

then A15: (H * x) * K c= (H * y) * K ;
for a being object st a in (H * y) * K holds
a in (H * x) * K

proof

let a be object ; :: thesis: ( a in (H * y) * K implies a in (H * x) * K )
assume a in (H * y) * K ; :: thesis: a in (H * x) * K
then consider h, k being Element of G such that
A16: a = (h * y) * k and
A17: h in H and
A18: k in K by Th17;
ex c, d being Element of G st
( a = (c * x) * d & c in H & d in K )

proof

h = h * (1_ G) by GROUP_1:def 4;
then A19: (h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k by GROUP_1:def 4;
1_ G = (h2 ") * h2 by GROUP_1:def 5;
then A20: (h * y) * k = (((h * ((h2 ") * h2)) * y) * (k2 * (k2 "))) * k by A19, GROUP_1:def 5
.= ((((h * ((h2 ") * h2)) * y) * k2) * (k2 ")) * k by GROUP_1:def 3
.= (((((h * (h2 ")) * h2) * y) * k2) * (k2 ")) * k by GROUP_1:def 3
.= ((((h * (h2 ")) * (h2 * y)) * k2) * (k2 ")) * k by GROUP_1:def 3
.= (((h * (h2 ")) * ((h1 * x) * k1)) * (k2 ")) * k by A3, A6, GROUP_1:def 3
.= ((((h * (h2 ")) * (h1 * x)) * k1) * (k2 ")) * k by GROUP_1:def 3
.= (((((h * (h2 ")) * h1) * x) * k1) * (k2 ")) * k by GROUP_1:def 3
.= ((((h * (h2 ")) * h1) * x) * (k1 * (k2 "))) * k by GROUP_1:def 3
.= (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) by GROUP_1:def 3 ;
take (h * (h2 ")) * h1 ; :: thesis: ex d being Element of G st
( a = (((h * (h2 ")) * h1) * x) * d & (h * (h2 ")) * h1 in H & d in K )
take (k1 * (k2 ")) * k ; :: thesis: ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K )
h2 " in H by A7, GROUP_2:51;
then A21: h * (h2 ") in H by A17, GROUP_2:50;
k2 " in K by A8, GROUP_2:51;
then k1 * (k2 ") in K by A5, GROUP_2:50;
hence ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K ) by A4, A16, A18, A20, A21, GROUP_2:50; :: thesis: verum

end;

hence a in (H * x) * K by Th17; :: thesis: verum

end;

then (H * y) * K c= (H * x) * K ;
hence ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) ) by A15, XBOOLE_0:def 10; :: thesis: verum

end;

end;