for L being RelStr
for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B