defpred S₁[ Element of MSSub U0, Element of MSSub U0, Element of MSSub U0] means for U1, U2 being strict MSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 "\/" U2;
A1: for x, y being Element of MSSub U0 ex z being Element of MSSub U0 st S₁[x,y,z]

proof

let x, y be Element of MSSub U0; :: thesis: ex z being Element of MSSub U0 st S₁[x,y,z]
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
reconsider z = U1 "\/" U2 as Element of MSSub U0 by Def19;
take z ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] ; :: thesis: verum

end;

consider o being BinOp of (MSSub U0) such that
A2: for a, b being Element of MSSub U0 holds S₁[a,b,o . (a,b)] from BINOP_1:sch 3(A1);
take o ; :: thesis: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/" U2
thus for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/" U2 by A2; :: thesis: verum