theorem :: FILTER_2:31

for L being Lattice st L is upper-bounded holds
(.L.> = (.(Top L).>