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;

consider o being BinOp of (Subgroups G) such that
A2: for a, b being Element of Subgroups G holds S₁[a,b,o . (a,b)] from BINOP_1:sch 3(A1);
take o ; :: thesis: for H1, H2 being strict Subgroup of G holds o . (H1,H2) = H1 "\/" H2
let H1, H2 be strict Subgroup of G; :: thesis: o . (H1,H2) = H1 "\/" H2
( H1 in Subgroups G & H2 in Subgroups G ) by GROUP_3:def 1;
hence o . (H1,H2) = H1 "\/" H2 by A2; :: thesis: verum