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