let G be Group; :: thesis: for a, b being Element of G

for H being Subgroup of G holds

( H * a = H * b iff H * a meets H * b )

let a, b be Element of G; :: thesis: for H being Subgroup of G holds

( H * a = H * b iff H * a meets H * b )

let H be Subgroup of G; :: thesis: ( H * a = H * b iff H * a meets H * b )

H * a <> {} by Th108;

hence ( H * a = H * b implies H * a meets H * b ) ; :: thesis: ( H * a meets H * b implies H * a = H * b )

assume H * a meets H * b ; :: thesis: H * a = H * b

then consider x being object such that

A1: x in H * a and

A2: x in H * b by XBOOLE_0:3;

reconsider x = x as Element of G by A2;

consider g being Element of G such that

A3: x = g * a and

A4: g in H by A1, Th104;

A5: g " in H by A4, Th51;

consider h being Element of G such that

A6: x = h * b and

A7: h in H by A2, Th104;

a = (g ") * (h * b) by A3, A6, GROUP_1:13

.= ((g ") * h) * b by GROUP_1:def 3 ;

then a * (b ") = (g ") * h by GROUP_1:14;

then a * (b ") in H by A7, A5, Th50;

hence H * a = H * b by Th120; :: thesis: verum

for H being Subgroup of G holds

( H * a = H * b iff H * a meets H * b )

let a, b be Element of G; :: thesis: for H being Subgroup of G holds

( H * a = H * b iff H * a meets H * b )

let H be Subgroup of G; :: thesis: ( H * a = H * b iff H * a meets H * b )

H * a <> {} by Th108;

hence ( H * a = H * b implies H * a meets H * b ) ; :: thesis: ( H * a meets H * b implies H * a = H * b )

assume H * a meets H * b ; :: thesis: H * a = H * b

then consider x being object such that

A1: x in H * a and

A2: x in H * b by XBOOLE_0:3;

reconsider x = x as Element of G by A2;

consider g being Element of G such that

A3: x = g * a and

A4: g in H by A1, Th104;

A5: g " in H by A4, Th51;

consider h being Element of G such that

A6: x = h * b and

A7: h in H by A2, Th104;

a = (g ") * (h * b) by A3, A6, GROUP_1:13

.= ((g ") * h) * b by GROUP_1:def 3 ;

then a * (b ") = (g ") * h by GROUP_1:14;

then a * (b ") in H by A7, A5, Th50;

hence H * a = H * b by Th120; :: thesis: verum