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 a' = a, b' = b, c' = 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 (b' ^ c')) by Def4
.= mi (a' ^ (mi (b' ^ c'))) by Def4
.= mi (a' ^ (b' ^ c')) by Th20
.= mi ((a' ^ b') ^ c') by Th21
.= mi ((mi (a' ^ b')) ^ c') by Th19
.= the L_meet of (SubstLatt V,C) . (mi (a' ^ b')),c' by Def4
.= (a "/\" b) "/\" c by Def4 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum