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

proof

assume A1: a + H = b + H ; :: thesis: (- b) + a in H
((- b) + a) + H = (- b) + (a + H) by Th32
.= ((- b) + b) + H by A1, Th32
.= (0_ G) + H by Def5
.= carr H by Th37 ;
hence (- b) + a in H by Th113; :: thesis: verum

end;

assume A2: (- b) + a in H ; :: thesis: a + H = b + H
thus a + H = (0_ G) + (a + H) by Th37
.= ((0_ G) + a) + H by Th32
.= ((b + (- b)) + a) + H by Def5
.= (b + ((- b) + a)) + H by RLVECT_1:def 3
.= b + (((- b) + a) + H) by Th32
.= b + H by A2, Th113 ; :: thesis: verum