set S1 = the discrete op-discrete OrderSortedSign;
take the discrete op-discrete OrderSortedSign ; :: thesis: ( the discrete op-discrete OrderSortedSign is locally_directed & the discrete op-discrete OrderSortedSign is regular )
thus ( the discrete op-discrete OrderSortedSign is locally_directed & the discrete op-discrete OrderSortedSign is regular ) ; :: thesis: verum