let V, C be set ; :: thesis: for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
let K, L, M be Element of SubstitutionSet (V,C); :: thesis: the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
A1: the L_meet of (SubstLatt (V,C)) . (K,M) = mi (K ^ M) by Def4;
( the L_join of (SubstLatt (V,C)) . (L,M) = mi (L \/ M) & the L_meet of (SubstLatt (V,C)) . (K,L) = mi (K ^ L) ) by Def4;
then reconsider La = the L_join of (SubstLatt (V,C)) . (L,M), Lb = the L_meet of (SubstLatt (V,C)) . (K,L), Lc = the L_meet of (SubstLatt (V,C)) . (K,M) as Element of SubstitutionSet (V,C) by A1;
the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = mi (K ^ La) by Def4
.= mi (K ^ (mi (L \/ M))) by Def4
.= mi (K ^ (L \/ M)) by Th20
.= mi ((K ^ L) \/ (K ^ M)) by Th22
.= mi ((mi (K ^ L)) \/ (K ^ M)) by Th13
.= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th13
.= mi (Lb \/ (mi (K ^ M))) by Def4
.= mi (Lb \/ Lc) by Def4 ;
hence the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) by Def4; :: thesis: verum