consider R being discrete OrderSortedSign;
take R ; :: thesis: R is locally_directed
thus R is locally_directed by Th9; :: thesis: verum