theorem :: FILTER_2:65

for L being Lattice
for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]