defpred S₁[ set , set , set ] means for H1, H2 being Subgroup of G st $1 = H1 & $2 = H2 holds
$3 = H1 "\/" H2;
A1: for S1, S2 being Element of Subgroups G ex B being Element of Subgroups G st S₁[S1,S2,B]

proof

let S1, S2 be Element of Subgroups G; :: thesis: ex B being Element of Subgroups G st S₁[S1,S2,B]
reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1;
reconsider C = H1 "\/" H2 as Element of Subgroups G by GROUP_3:def 1;
take C ; :: thesis: S₁[S1,S2,C]
thus S₁[S1,S2,C] ; :: thesis: verum

end;

ex o being BinOp of Subgroups G st
for a, b being Element of Subgroups G holds S₁[a,b,o . a,b] from BINOP_1:sch 3(A1);
hence ex b₁ being BinOp of Subgroups G st
for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b₁ . S1,S2 = H1 "\/" H2 ; :: thesis: verum