let G be Group; :: thesis: for H1, H2 being Subgroup of G
for g being Element of G st ( g in H1 or g in H2 ) holds
g in H1 "\/" H2
let H1, H2 be Subgroup of G; :: thesis: for g being Element of G st ( g in H1 or g in H2 ) holds
g in H1 "\/" H2
let g be Element of G; :: thesis: ( ( g in H1 or g in H2 ) implies g in H1 "\/" H2 )
assume A1: ( g in H1 or g in H2 ) ; :: thesis: g in H1 "\/" H2

now :: thesis: g in H1 "\/" H2

per cases ( g in H1 or g in H2 ) by A1;

suppose A2: g in H1 ; :: thesis: g in H1 "\/" H2

( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by GROUP_2:def 5;
then reconsider A = the carrier of H1 \/ the carrier of H2 as Subset of G by XBOOLE_1:8;
g in the carrier of H1 by A2, STRUCT_0:def 5;
then g in A by XBOOLE_0:def 3;
then g in gr A by GROUP_4:29;
hence g in H1 "\/" H2 by Th4; :: thesis: verum

end;

suppose A3: g in H2 ; :: thesis: g in H1 "\/" H2

( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by GROUP_2:def 5;
then reconsider A = the carrier of H1 \/ the carrier of H2 as Subset of G by XBOOLE_1:8;
g in the carrier of H2 by A3, STRUCT_0:def 5;
then g in A by XBOOLE_0:def 3;
then g in gr A by GROUP_4:29;
hence g in H1 "\/" H2 by Th4; :: thesis: verum

end;

end;

end;

hence g in H1 "\/" H2 ; :: thesis: verum