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 Th108;
hence ( a * H = b * H implies a * H meets b * H ) ; :: 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 object 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 and
A4: g in H by A1, Th103;
A5: g " in H by A4, Th51;
consider h being Element of G such that
A6: x = b * h and
A7: h in H by A2, Th103;
a = (b * h) * (g ") by A3, A6, GROUP_1:14
.= b * (h * (g ")) by GROUP_1:def 3 ;
then (b ") * a = h * (g ") by GROUP_1:13;
then (b ") * a in H by A7, A5, Th50;
hence a * H = b * H by Th114; :: thesis: verum