let A be set ; :: thesis: for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . K,(the L_join of (NormForm A) . L,M) = the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),(the L_meet of (NormForm A) . K,M)
let K, L, M be Element of Normal_forms_on A; :: thesis: the L_meet of (NormForm A) . K,(the L_join of (NormForm A) . L,M) = the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),(the L_meet of (NormForm A) . K,M)
( the L_join of (NormForm A) . L,M = mi (L \/ M) & the L_meet of (NormForm A) . K,L = mi (K ^ L) & the L_meet of (NormForm A) . K,M = mi (K ^ M) ) by Def14;
then reconsider La = the L_join of (NormForm A) . L,M, Lb = the L_meet of (NormForm A) . K,L, Lc = the L_meet of (NormForm A) . K,M as Element of Normal_forms_on A ;
the L_meet of (NormForm A) . K,(the L_join of (NormForm A) . L,M) = mi (K ^ La) by Def14
.= mi (K ^ (mi (L \/ M))) by Def14
.= mi (K ^ (L \/ M)) by Th75
.= mi ((K ^ L) \/ (K ^ M)) by Th77
.= mi ((mi (K ^ L)) \/ (K ^ M)) by Th68
.= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th68
.= mi (Lb \/ (mi (K ^ M))) by Def14
.= mi (Lb \/ Lc) by Def14 ;
hence the L_meet of (NormForm A) . K,(the L_join of (NormForm A) . L,M) = the L_join of (NormForm A) . (the L_meet of (NormForm A) . K,L),(the L_meet of (NormForm A) . K,M) by Def14; :: thesis: verum