for N being transitive RelStr
for A, J being Subset of N st A is_coarser_than uparrow J holds
uparrow A c= uparrow J