consider S1 being discrete op-discrete OrderSortedSign;
take S1 ; :: thesis: ( S1 is locally_directed & S1 is regular )
thus ( S1 is locally_directed & S1 is regular ) ; :: thesis: verum