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