theorem Th26: :: YELLOW_7:26

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