theorem :: LATTICE2:66

for A being non empty set
for B being Element of Fin A
for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds u "/\" (FinJoin (B,f)) = FinJoin (B,( the L_meet of L [;] (u,f))) by Th64;