theorem :: FILTER_2:66
for L being Lattice
for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]