theorem :: FILTER_2:39

for L being Lattice
for p being Element of L
for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>