let A be set ; :: thesis: for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),L = L
let K, L be Element of Normal_forms_on A; :: thesis: the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),L = L
thus the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),L = the L_join of (NormForm A) . (mi (K ^ L)),L by Def14
.= mi ((mi (K ^ L)) \/ L) by Def14
.= mi ((K ^ L) \/ L) by Th68
.= mi L by Lm8
.= L by Th66 ; :: thesis: verum