defpred S_{1}[ 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_{1}[x,y,z]

A2: for a, b being Element of MSSub U0 holds S_{1}[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

$3 = U1 /\ U2;

A1: for x, y being Element of MSSub U0 ex z being Element of MSSub U0 st S

proof

consider o being BinOp of (MSSub U0) such that
let x, y be Element of MSSub U0; :: thesis: ex z being Element of MSSub U0 st S_{1}[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_{1}[x,y,z]

thus S_{1}[x,y,z]
; :: thesis: verum

end;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

thus S

A2: for a, b being Element of MSSub U0 holds S

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