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