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:31;
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 Th43
.= (MSAlg_meet U0) . (y,x) by A1, BINOP_1:def 2
.= (OSAlg_meet U0) . (y,x) by Th43 ;
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