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

proof

let x, y be Element of OSSub U0; :: thesis: (OSAlg_meet U0) . x,y = (OSAlg_meet U0) . y,x
(OSAlg_meet U0) . x,y = (MSAlg_meet U0) . x,y by Th48
.= (MSAlg_meet U0) . y,x by A1, BINOP_1:def 2
.= (OSAlg_meet U0) . y,x by Th48 ;
hence (OSAlg_meet U0) . x,y = (OSAlg_meet U0) . y,x ; :: thesis: verum

end;

hence OSAlg_meet U0 is commutative by BINOP_1:def 2; :: thesis: verum