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