let V, C be set ; 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); 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; verum