for L being non empty RelStr
for p, x being Element of L holds
( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p )