theorem :: FILTER_0:61

for L being Lattice
for p, q being Element of L holds p <=> q = q <=> p ;