Order induced by restriction

	new file:   Order.agda