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 Def12

.= mi ((mi (K ^ L)) \/ L) by Def12

.= mi ((K ^ L) \/ L) by Th44

.= mi L by Lm8

.= L by Th42 ; :: thesis: verum

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 Def12

.= mi ((mi (K ^ L)) \/ L) by Def12

.= mi ((K ^ L) \/ L) by Th44

.= mi L by Lm8

.= L by Th42 ; :: thesis: verum