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 & z in (H * y) * K ) ;
consider h1, k1 being Element of G such that
A2: ( z = (h1 * x) * k1 & h1 in H & k1 in K ) by A1, Th17;
consider h2, k2 being Element of G such that
A3: ( z = (h2 * y) * k2 & h2 in H & k2 in K ) by A1, Th17;
A4: (H * x) * K c= (H * y) * K

proof

for a being set st a in (H * x) * K holds
a in (H * y) * K

proof

let a be set ; :: 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
A5: ( a = (h * x) * k & h in H & 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 5;
then A6: (h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k by GROUP_1:def 5;
1_ G = (h1 " ) * h1 by GROUP_1:def 6;
then A7: (h * x) * k = (((h * ((h1 " ) * h1)) * x) * (k1 * (k1 " ))) * k by A6, GROUP_1:def 6
.= ((((h * ((h1 " ) * h1)) * x) * k1) * (k1 " )) * k by GROUP_1:def 4
.= (((((h * (h1 " )) * h1) * x) * k1) * (k1 " )) * k by GROUP_1:def 4
.= ((((h * (h1 " )) * (h1 * x)) * k1) * (k1 " )) * k by GROUP_1:def 4
.= (((h * (h1 " )) * ((h2 * y) * k2)) * (k1 " )) * k by A2, A3, GROUP_1:def 4
.= ((((h * (h1 " )) * (h2 * y)) * k2) * (k1 " )) * k by GROUP_1:def 4
.= (((((h * (h1 " )) * h2) * y) * k2) * (k1 " )) * k by GROUP_1:def 4
.= ((((h * (h1 " )) * h2) * y) * (k2 * (k1 " ))) * k by GROUP_1:def 4
.= (((h * (h1 " )) * h2) * y) * ((k2 * (k1 " )) * k) by GROUP_1:def 4 ;
take c = (h * (h1 " )) * h2; :: thesis: ex d being Element of G st
( a = (c * y) * d & c in H & d in K )
take d = (k2 * (k1 " )) * k; :: thesis: ( a = (c * y) * d & c in H & d in K )
A8: (h * (h1 " )) * h2 in H

proof

( h in H & h1 " in H ) by A2, A5, GROUP_2:60;
then h * (h1 " ) in H by GROUP_2:59;
hence (h * (h1 " )) * h2 in H by A3, GROUP_2:59; :: thesis: verum

end;

(k2 * (k1 " )) * k in K

proof

( k2 in K & k1 " in K ) by A2, A3, GROUP_2:60;
then k2 * (k1 " ) in K by GROUP_2:59;
hence (k2 * (k1 " )) * k in K by A5, GROUP_2:59; :: thesis: verum

end;

hence ( a = (c * y) * d & c in H & d in K ) by A5, A7, A8; :: thesis: verum

end;

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

end;

hence (H * x) * K c= (H * y) * K by TARSKI:def 3; :: thesis: verum

end;

(H * y) * K c= (H * x) * K

proof

for a being set st a in (H * y) * K holds
a in (H * x) * K

proof

let a be set ; :: 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
A9: ( a = (h * y) * k & h in H & 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 5;
then A10: (h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k by GROUP_1:def 5;
1_ G = (h2 " ) * h2 by GROUP_1:def 6;
then A11: (h * y) * k = (((h * ((h2 " ) * h2)) * y) * (k2 * (k2 " ))) * k by A10, GROUP_1:def 6
.= ((((h * ((h2 " ) * h2)) * y) * k2) * (k2 " )) * k by GROUP_1:def 4
.= (((((h * (h2 " )) * h2) * y) * k2) * (k2 " )) * k by GROUP_1:def 4
.= ((((h * (h2 " )) * (h2 * y)) * k2) * (k2 " )) * k by GROUP_1:def 4
.= (((h * (h2 " )) * ((h1 * x) * k1)) * (k2 " )) * k by A2, A3, GROUP_1:def 4
.= ((((h * (h2 " )) * (h1 * x)) * k1) * (k2 " )) * k by GROUP_1:def 4
.= (((((h * (h2 " )) * h1) * x) * k1) * (k2 " )) * k by GROUP_1:def 4
.= ((((h * (h2 " )) * h1) * x) * (k1 * (k2 " ))) * k by GROUP_1:def 4
.= (((h * (h2 " )) * h1) * x) * ((k1 * (k2 " )) * k) by GROUP_1:def 4 ;
take c = (h * (h2 " )) * h1; :: thesis: ex d being Element of G st
( a = (c * x) * d & c in H & d in K )
take d = (k1 * (k2 " )) * k; :: thesis: ( a = (c * x) * d & c in H & d in K )
A12: (h * (h2 " )) * h1 in H

proof

( h in H & h2 " in H ) by A3, A9, GROUP_2:60;
then h * (h2 " ) in H by GROUP_2:59;
hence (h * (h2 " )) * h1 in H by A2, GROUP_2:59; :: thesis: verum

end;

(k1 * (k2 " )) * k in K

proof

( k1 in K & k2 " in K ) by A2, A3, GROUP_2:60;
then k1 * (k2 " ) in K by GROUP_2:59;
hence (k1 * (k2 " )) * k in K by A9, GROUP_2:59; :: thesis: verum

end;

hence ( a = (c * x) * d & c in H & d in K ) by A9, A11, A12; :: thesis: verum

end;

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

end;

hence (H * y) * K c= (H * x) * K by TARSKI:def 3; :: thesis: verum

end;

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 A4, XBOOLE_0:def 10; :: thesis: verum

end;

end;