Proved that djoin is a join in the lattice-theoretic sense.
	modified:   RestrictionDelay.agda