theorem Th23: :: UNIALG_2:23

for U0 being with_const_op Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2