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 Lm8 ; :: thesis: verum