for L being distributive Lattice
for a, b being Element of L holds (PrimeFilters L) . (a "/\" b) = ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b)