theorem Th46: :: OSALG_2:46

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative