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

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a + H or x in carr H )
assume x in a + H ; :: thesis: x in carr H
then consider g being Element of G such that
A2: x = a + g and
A3: g in H by Th103;
a + g in H by A1, A3, Th50;
hence x in carr H by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in carr H or x in a + H )
assume A4: x in carr H ; :: thesis: x in a + H
then A5: x in H ;
reconsider b = x as Element of G by A4;
A6: a + ((- a) + b) = (a + (- a)) + b by RLVECT_1:def 3
.= (0_ G) + b by Def5
.= x by Def4 ;
- a in H by A1, Th51;
hence x in a + H by A5, A6, Th50, Th103; :: thesis: verum

end;

assume A7: a + H = carr H ; :: thesis: a in H
( a + (0_ G) = a & 0_ G in H ) by Th46, Def4;
hence a in H by A7, Th103; :: thesis: verum