theorem :: FILTER_0:13

for L being Lattice
for p being Element of L st {p} is Filter of L holds
L is upper-bounded