let G be addGroup; :: thesis: 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; :: thesis: for H being Subgroup of G holds
( a + H = b + H iff a + H meets b + H )
let H be Subgroup of G; :: thesis: ( a + H = b + H iff a + H meets b + H )
thus ( a + H = b + H implies a + H meets b + H ) by Th108; :: thesis: ( a + H meets b + H implies a + H = b + H )
assume a + H meets b + H ; :: thesis: 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; :: thesis: verum