theorem :: HEYTING3:11

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))