let V, C be set ; :: thesis: for K, L being Element of SubstitutionSet V,C holds the L_join of (SubstLatt V,C) . (the L_meet of (SubstLatt V,C) . K,L),L = L
let K, L be Element of SubstitutionSet V,C; :: thesis: the L_join of (SubstLatt V,C) . (the L_meet of (SubstLatt V,C) . K,L),L = L
thus the L_join of (SubstLatt V,C) . (the L_meet of (SubstLatt V,C) . K,L),L = the L_join of (SubstLatt V,C) . (mi (K ^ L)),L by Def4
.= mi ((mi (K ^ L)) \/ L) by Def4
.= mi ((K ^ L) \/ L) by Th13
.= mi L by Lm5
.= L by Th11 ; :: thesis: verum