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

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