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 that
A1: H1 is Subgroup of H3 and
A2: H2 is Subgroup of H3 ; :: thesis: H1 "\/" H2 is Subgroup of H3

now

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
A3: ( len F = len I & rng F c= (carr H1) \/ (carr H2) & a = Product (F |^ I) ) by Th37;
( the carrier of H1 c= the carrier of H3 & the carrier of H2 c= the carrier of H3 & the carrier of H1 = carr H1 & the carrier of H2 = carr H2 & the carrier of H3 = carr H3 ) by A1, A2, GROUP_2:def 5;
then (carr H1) \/ (carr H2) c= carr H3 by XBOOLE_1:8;
then rng F c= carr H3 by A3, XBOOLE_1:1;
then a in gr (carr H3) by A3, Th37;
hence a in H3 by Th40; :: thesis: verum

end;

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