let V, C be set ; :: thesis: for a, b being Element of (SubstLatt V,C) holds a "/\" (a "\/" b) = a
let a, b be Element of (SubstLatt V,C); :: thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of SubstitutionSet V,C by Def4;
thus a "/\" (a "\/" b) = the L_join of (SubstLatt V,C) . (the L_meet of (SubstLatt V,C) . a9,a9),(the L_meet of (SubstLatt V,C) . a9,b9) by Lm12
.= the L_join of (SubstLatt V,C) . (mi (a9 ^ a9)),(the L_meet of (SubstLatt V,C) . a9,b9) by Def4
.= the L_join of (SubstLatt V,C) . (mi a9),(the L_meet of (SubstLatt V,C) . a9,b9) by Th24
.= a "\/" (a "/\" b) by Th11
.= (a "/\" b) "\/" a by Lm6
.= (b "/\" a) "\/" a by Lm10
.= a by Lm9 ; :: thesis: verum