theorem :: LATTICEA:27

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