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)))

A1: the L_meet of (NormForm A) . (K,M) = mi (K ^ M) by Def12;

( the L_join of (NormForm A) . (L,M) = mi (L \/ M) & the L_meet of (NormForm A) . (K,L) = mi (K ^ L) ) by Def12;

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 by A1;

the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = mi (K ^ La) by Def12

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

.= mi (K ^ (L \/ M)) by Th51

.= mi ((K ^ L) \/ (K ^ M)) by Th53

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

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

.= mi (Lb \/ (mi (K ^ M))) by Def12

.= mi (Lb \/ Lc) by Def12 ;

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 Def12; :: thesis: verum

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)))

A1: the L_meet of (NormForm A) . (K,M) = mi (K ^ M) by Def12;

( the L_join of (NormForm A) . (L,M) = mi (L \/ M) & the L_meet of (NormForm A) . (K,L) = mi (K ^ L) ) by Def12;

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 by A1;

the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = mi (K ^ La) by Def12

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

.= mi (K ^ (L \/ M)) by Th51

.= mi ((K ^ L) \/ (K ^ M)) by Th53

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

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

.= mi (Lb \/ (mi (K ^ M))) by Def12

.= mi (Lb \/ Lc) by Def12 ;

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 Def12; :: thesis: verum