set R = the non empty discrete Poset;
take the non empty discrete Poset ; :: thesis: the non empty discrete Poset is locally_directed
thus the non empty discrete Poset is locally_directed by Th8; :: thesis: verum