let G be Group; :: thesis: for H1, H2 being Subgroup of G
for A being Subset of G st A = the carrier of H1 \/ the carrier of H2 holds
H1 "\/" H2 = gr A
let H1, H2 be Subgroup of G; :: thesis: for A being Subset of G st A = the carrier of H1 \/ the carrier of H2 holds
H1 "\/" H2 = gr A
A1: the carrier of H2 = carr H2 by GROUP_2:def 9;
let A be Subset of G; :: thesis: ( A = the carrier of H1 \/ the carrier of H2 implies H1 "\/" H2 = gr A )
assume A = the carrier of H1 \/ the carrier of H2 ; :: thesis: H1 "\/" H2 = gr A
hence H1 "\/" H2 = gr A by A1, GROUP_2:def 9; :: thesis: verum