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

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

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

then A2: g in the carrier of H1 by STRUCT_0:def 5;
( 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 A by A2, XBOOLE_0:def 3;
then g in gr A by GROUP_4:38;
hence g in H1 "\/" H2 by Th4; :: thesis: verum

end;

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

then A3: g in the carrier of H2 by STRUCT_0:def 5;
( 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 A by A3, XBOOLE_0:def 3;
then g in gr A by GROUP_4:38;
hence g in H1 "\/" H2 by Th4; :: thesis: verum

end;

end;

end;

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