theorem Th63: :: FOMODEL0:63

for A, B being set st B is c=directed & A is_finer_than B holds
A \/ B is c=directed