theorem :: FILTER_2:63

for L being Lattice
for p, q being Element of L st p [= q holds
( p in [#p,q#] & q in [#p,q#] ) by Th62;