let G be addGroup; :: thesis: for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) + a = (H1 + a) /\ (H2 + a)
let a be Element of G; :: thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) + a = (H1 + a) /\ (H2 + a)
let H1, H2 be Subgroup of G; :: thesis: (H1 /\ H2) + a = (H1 + a) /\ (H2 + a)
thus (H1 /\ H2) + a c= (H1 + a) /\ (H2 + a) :: according to XBOOLE_0:def 10 :: thesis: (H1 + a) /\ (H2 + a) c= (H1 /\ H2) + a

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 /\ H2) + a or x in (H1 + a) /\ (H2 + a) )
assume x in (H1 /\ H2) + a ; :: thesis: x in (H1 + a) /\ (H2 + a)
then consider g being Element of G such that
A1: x = g + a and
A2: g in H1 /\ H2 by Th104;
g in H2 by A2, Th82;
then A3: x in H2 + a by A1, Th104;
g in H1 by A2, Th82;
then x in H1 + a by A1, Th104;
hence x in (H1 + a) /\ (H2 + a) by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 + a) /\ (H2 + a) or x in (H1 /\ H2) + a )
assume A4: x in (H1 + a) /\ (H2 + a) ; :: thesis: x in (H1 /\ H2) + a
then x in H1 + a by XBOOLE_0:def 4;
then consider g being Element of G such that
A5: x = g + a and
A6: g in H1 by Th104;
x in H2 + a by A4, XBOOLE_0:def 4;
then consider g1 being Element of G such that
A7: x = g1 + a and
A8: g1 in H2 by Th104;
g = g1 by A5, A7, Th6;
hence x in (H1 /\ H2) + a by A5, A6, A8, Th82, Th104; :: thesis: verum