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

proof

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

end;

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