let G be addGroup; for a, b being Element of G
for H being Subgroup of G holds
( a + H = b + H iff a + H meets b + H )
let a, b be Element of G; for H being Subgroup of G holds
( a + H = b + H iff a + H meets b + H )
let H be Subgroup of G; ( a + H = b + H iff a + H meets b + H )
thus
( a + H = b + H implies a + H meets b + H )
by Th108; ( a + H meets b + H implies a + H = b + H )
assume
a + H meets b + H
; a + H = b + H
then consider x being object such that
A1:
x in a + H
and
A2:
x in b + H
by XBOOLE_0:3;
reconsider x = x as Element of G by A2;
consider g being Element of G such that
A3:
x = a + g
and
A4:
g in H
by A1, Th103;
A5:
- g in H
by A4, Th51;
consider h being Element of G such that
A6:
x = b + h
and
A7:
h in H
by A2, Th103;
a =
(b + h) + (- g)
by A3, A6, Th13
.=
b + (h + (- g))
by RLVECT_1:def 3
;
then
(- b) + a = h + (- g)
by Th12;
hence
a + H = b + H
by A5, A7, Th50, Th114; verum