let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
let U0 be non-empty OSAlgebra of S1; :: thesis: OSAlg_meet U0 is associative
set o = OSAlg_meet U0;
set m = MSAlg_meet U0;
A1: MSAlg_meet U0 is associative by MSUALG_2:32;
for x, y, z being Element of OSSub U0 holds (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)

proof

let x, y, z be Element of OSSub U0; :: thesis: (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
A2: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43;
(OSAlg_meet U0) . (y,z) = (MSAlg_meet U0) . (y,z) by Th43;
then (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) by Th43
.= (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A1, BINOP_1:def 3
.= (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) by A2, Th43 ;
hence (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) ; :: thesis: verum

end;

hence OSAlg_meet U0 is associative by BINOP_1:def 3; :: thesis: verum