theorem Th7: :: YELLOW_2:7

for X being set
for L being non empty RelStr
for S being non empty SubRelStr of L holds
( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )