let G be Group; :: thesis:
let H1, H2 be Subgroup of G; :: thesis:
let H3 be strict Subgroup of G; :: thesis:
assume A1: ( H1 is Subgroup of H3 & H2 is Subgroup of H3 ) ; :: thesis:

let a be Element of G; :: thesis:
assume a in H1 "\/" H2 ; :: thesis:
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:

end;