let V, C be set ; :: thesis: for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b
let a, b be Element of (SubstLatt (V,C)); :: thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
thus (a "/\" b) "\/" b = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,b9)),b9)
.= b by Lm7 ; :: thesis: verum