let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds
( a in H iff H * a = carr H )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( a in H iff H * a = carr H )
let H be Subgroup of G; :: thesis: ( a in H iff H * a = carr H )
thus ( a in H implies H * a = carr H ) :: thesis: ( H * a = carr H implies a in H )

proof

assume A1: a in H ; :: thesis: H * a = carr H
thus H * a c= carr H :: according to XBOOLE_0:def 10 :: thesis: carr H c= H * a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H * a or x in carr H )
assume x in H * a ; :: thesis: x in carr H
then consider g being Element of G such that
A2: x = g * a and
A3: g in H by Th126;
g * a in H by A1, A3, Th59;
hence x in carr H by A2, STRUCT_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in carr H or x in H * a )
assume A4: x in carr H ; :: thesis: x in H * a
then A5: x in H by STRUCT_0:def 5;
reconsider b = x as Element of G by A4;
a " in H by A1, Th60;
then A6: b * (a " ) in H by A5, Th59;
(b * (a " )) * a = b * ((a " ) * a) by GROUP_1:def 4
.= b * (1_ G) by GROUP_1:def 6
.= x by GROUP_1:def 5 ;
hence x in H * a by A6, Th126; :: thesis: verum

end;

assume A7: H * a = carr H ; :: thesis: a in H
( (1_ G) * a = a & 1_ G in H ) by Th55, GROUP_1:def 5;
then a in carr H by A7, Th126;
hence a in H by STRUCT_0:def 5; :: thesis: verum