theorem Th7: :: LATTICE3:7

for L being Lattice
for p, q being Element of L holds
( p [= q iff p % <= q % ) by FILTER_1:31;