:: deftheorem defines LOWER LATTICE7:def 7 :
for P being RelStr holds LOWER P = { X where X is Subset of P : X is lower } ;