theorem Th22: :: UNIALG_2:22

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