theorem :: COHSP_1:15

for X being non empty set st X includes_lattice_of X holds
( X is c=directed & X is c=filtered )