let G be Group; :: thesis: for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff a * H meets b * H )
let a, b be Element of G; :: thesis: for H being Subgroup of G holds
( a * H = b * H iff a * H meets b * H )
let H be Subgroup of G; :: thesis: ( a * H = b * H iff a * H meets b * H )
a * H <> {} by Th130;
hence ( a * H = b * H implies a * H meets b * H ) by XBOOLE_1:66; :: thesis: ( a * H meets b * H implies a * H = b * H )
assume a * H meets b * H ; :: thesis: a * H = b * H
then consider x being set such that
A1: x in a * H and
A2: x in b * H by XBOOLE_0:3;
reconsider x = x as Element of G by A2;
consider g being Element of G such that
A3: ( x = a * g & g in H ) by A1, Th125;
consider h being Element of G such that
A4: ( x = b * h & h in H ) by A2, Th125;
a = (b * h) * (g " ) by A3, A4, GROUP_1:22
.= b * (h * (g " )) by GROUP_1:def 4 ;
then A5: (b " ) * a = h * (g " ) by GROUP_1:21;
g " in H by A3, Th60;
then (b " ) * a in H by A4, A5, Th59;
hence a * H = b * H by Th137; :: thesis: verum