let G be Group; :: thesis: for H1, H2 being Subgroup of G
for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds
H1 "\/" H2 is Subgroup of H3
let H1, H2 be Subgroup of G; :: thesis: for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds
H1 "\/" H2 is Subgroup of H3
let H3 be strict Subgroup of G; :: thesis: ( H1 is Subgroup of H3 & H2 is Subgroup of H3 implies H1 "\/" H2 is Subgroup of H3 )
assume A1: ( H1 is Subgroup of H3 & H2 is Subgroup of H3 ) ; :: thesis: H1 "\/" H2 is Subgroup of H3

now :: thesis: for a being Element of G st a in H1 "\/" H2 holds
a in H3

let a be Element of G; :: thesis: ( a in H1 "\/" H2 implies a in H3 )
assume a in H1 "\/" H2 ; :: thesis: a in H3
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A2: len F = len I and
A3: rng F c= (carr H1) \/ (carr H2) and
A4: a = Product (F |^ I) by Th28;
( the carrier of H1 c= the carrier of H3 & the carrier of H2 c= the carrier of H3 ) by A1, GROUP_2:def 5;
then (carr H1) \/ (carr H2) c= carr H3 by XBOOLE_1:8;
then rng F c= carr H3 by A3;
then a in gr (carr H3) by A2, A4, Th28;
hence a in H3 by Th31; :: thesis: verum

end;

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