theorem :: WAYBEL12:3

for L being non empty transitive RelStr
for A, B being Subset of L st A is_finer_than B holds
downarrow A c= downarrow B