theorem Th62: :: FILTER_2:62

for L being Lattice
for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r & r [= q ) )