theorem Th41: :: OSALG_2:41

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2