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