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:33;
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 Th48;
(OSAlg_meet U0) . y,z = (MSAlg_meet U0) . y,z by Th48;
then (OSAlg_meet U0) . x,((OSAlg_meet U0) . y,z) = (MSAlg_meet U0) . x,((MSAlg_meet U0) . y,z) by Th48
.= (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, Th48 ;
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