theorem :: FILTER_0:3

for L being Lattice
for p, q, r being Element of L st p [= r holds
p [= q "\/" r