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 Th130;
hence ( H * a = H * b implies H * a meets H * b ) by XBOOLE_1:66; :: 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 set 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, Th126;
A5: g " in H by A4, Th60;
consider h being Element of G such that
A6: x = h * b and
A7: h in H by A2, Th126;
a = (g ") * (h * b) by A3, A6, GROUP_1:21
.= ((g ") * h) * b by GROUP_1:def 4 ;
then a * (b ") = (g ") * h by GROUP_1:22;
then a * (b ") in H by A7, A5, Th59;
hence H * a = H * b by Th143; :: thesis: verum