let V, C be set ; :: thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
let a, b, c be Element of (SubstLatt (V,C)); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
a "/\" (b "/\" c) = the L_meet of (SubstLatt (V,C)) . (a,(mi (b9 ^ c9))) by Def4
.= mi (a9 ^ (mi (b9 ^ c9))) by Def4
.= mi (a9 ^ (b9 ^ c9)) by Th20
.= mi ((a9 ^ b9) ^ c9) by Th21
.= mi ((mi (a9 ^ b9)) ^ c9) by Th19
.= the L_meet of (SubstLatt (V,C)) . ((mi (a9 ^ b9)),c9) by Def4
.= (a "/\" b) "/\" c by Def4 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum