consider R being non empty discrete Poset;
take R ; :: thesis: R is locally_directed
thus R is locally_directed by Th9; :: thesis: verum