for L being RelStr
for x being set holds
( x is directed Subset of (L opp) iff x is filtered Subset of L )