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 Lm4
.= L by Th11 ; :: thesis: verum