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 :: thesis: for a being Element of G st a in (H1 "\/" H2) "\/" H3 holds
a in H1 "\/" (H2 "\/" H3)

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 Th28;
rng F c= carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))

proof

let x be object ; :: 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 :: thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))

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 reconsider b = x as Element of G ;
x in H1 "\/" H2 by A5, STRUCT_0:def 5;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A6: len F1 = len I1 and
A7: rng F1 c= (carr H1) \/ (carr H2) and
A8: b = Product (F1 |^ I1) by Th28;
H2 is Subgroup of H2 "\/" H3 by Lm4;
then the carrier of H2 c= the carrier of (H2 "\/" 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 A7;
then b in H1 "\/" (H2 "\/" H3) by A6, A8, Th28;
hence x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by STRUCT_0:def 5; :: thesis: verum

end;

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

A10: H3 is Subgroup of H3 "\/" H2 by Lm4;
x in H3 by A9, STRUCT_0:def 5;
then x in H3 "\/" H2 by A10, GROUP_2:40;
then x in carr (H2 "\/" H3) by STRUCT_0:def 5;
then A11: x in (carr H1) \/ (carr (H2 "\/" H3)) by XBOOLE_0:def 3;
(carr H1) \/ (carr (H2 "\/" H3)) c= the carrier of (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by Def4;
hence x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by A11; :: 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, Th28;
hence a in H1 "\/" (H2 "\/" H3) by Th31; :: thesis: verum

end;

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