let G be Group; :: thesis: for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
let H1, H2, H3 be Subgroup of G; :: thesis: (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)

now

let a be Element of G; :: thesis: ( a in (H1 "\/" H2) "\/" H3 implies a in H1 "\/" (H2 "\/" H3) )
assume a in (H1 "\/" H2) "\/" H3 ; :: thesis: a in H1 "\/" (H2 "\/" H3)
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A1: len F = len I and
A2: rng F c= (carr (H1 "\/" H2)) \/ (carr H3) and
A3: a = Product (F |^ I) by Th37;
rng F c= carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) )
assume A4: x in rng F ; :: thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))

now

per cases ( x in carr (H1 "\/" H2) or x in carr H3 ) by A2, A4, XBOOLE_0:def 3;

suppose A5: x in carr (H1 "\/" H2) ; :: thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))

then A6: x in H1 "\/" H2 by STRUCT_0:def 5;
reconsider b = x as Element of G by A5;
consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A7: len F1 = len I1 and
A8: rng F1 c= (carr H1) \/ (carr H2) and
A9: b = Product (F1 |^ I1) by A6, Th37;
H2 is Subgroup of H2 "\/" H3 by Lm4;
then ( the carrier of H2 c= the carrier of (H2 "\/" H3) & the carrier of H2 = carr H2 & the carrier of H3 = carr H3 & H2 "\/" H3 = gr ((carr H2) \/ (carr H3)) ) by GROUP_2:def 5;
then (carr H1) \/ (carr H2) c= (carr H1) \/ (carr (H2 "\/" H3)) by XBOOLE_1:9;
then rng F1 c= (carr H1) \/ (carr (H2 "\/" H3)) by A8, XBOOLE_1:1;
then b in H1 "\/" (H2 "\/" H3) by A7, A9, Th37;
hence x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by STRUCT_0:def 5; :: thesis: verum

end;

suppose x in carr H3 ; :: thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))

then ( x in H3 & H3 is Subgroup of H3 "\/" H2 ) by Lm4, STRUCT_0:def 5;
then x in H3 "\/" H2 by GROUP_2:49;
then x in carr (H2 "\/" H3) by STRUCT_0:def 5;
then ( x in (carr H1) \/ (carr (H2 "\/" H3)) & (carr H1) \/ (carr (H2 "\/" H3)) c= the carrier of (gr ((carr H1) \/ (carr (H2 "\/" H3)))) ) by Def5, XBOOLE_0:def 3;
hence x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) ; :: thesis: verum

end;

end;

end;

hence x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) ; :: thesis: verum

end;

then a in gr (carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))) by A1, A3, Th37;
hence a in H1 "\/" (H2 "\/" H3) by Th40; :: thesis: verum

end;

hence (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by GROUP_2:67; :: thesis: verum