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