set R = the discrete OrderSortedSign;
take the discrete OrderSortedSign ; :: thesis: the discrete OrderSortedSign is locally_directed
thus the discrete OrderSortedSign is locally_directed by Th8; :: thesis: verum